docs: reorganise -- current reference gathered, finished work archived, superseded and dead ideas marked as such
docs/CLAUDE.md Phase 2, 2026-10-14. All moves by git mv; every archived file carries a header saying what it is, why, and where to look instead. - docs/reference/ (new): roadmap and versioning policy, M7.1, word-ACL design, kernel args, hosted acceptance test, dictionary, primitives, ontology, L8 table -- previously spread over docs/, docs/lithosananke/ and docs/03-architecture/. - docs/working/archive/historical/: finished work (session plan, test-gap audit, birthing plan, fix write-ups, the January architecture draft). - docs/working/archive/superseded/: the Hermes-VM Tripod docs and July Hermes designs (-> FABRIC-3.5/3.6), the StarForth roadmap, every working doc already flagged superseded or obsolete. - docs/working/archive/dead/: the hal_* target contract (never adopted), L4Re, metrics-and-knobs. - Papers and proposals into docs/working/papers/. - References rewritten across the repo (not logs/, not docs/patent/); CLAUDE.md's documentation section rewritten. Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com>
This commit is contained in:
rajames
co-authored by
Claude Opus 5.5
Claude Opus 5.5
parent
1a4b163861
commit
7aed588f78
@@ -1,19 +0,0 @@
|
||||
# docs/03-architecture/
|
||||
|
||||
Architecture-constraint documents for LithosAnanke subsystems that are still
|
||||
being designed or built. These are binding constraints for anyone (human or
|
||||
Claude Code) touching the affected code, not general background reading.
|
||||
|
||||
- **[tripod/](tripod/)** — Architectural contracts for the three Tripod VMs
|
||||
(Hera, Hermes, Artemis): roles, dispatch rules, the compudynamic K≡1.0
|
||||
invariant, and explicit prohibitions.
|
||||
- **[word-acl/](word-acl/)** — Design doc for the word-level ACL system
|
||||
(`capsules/ACL.4th`, `capsules/zuse.4th`, `src/word_source/acl_words.c`).
|
||||
|
||||
## See also
|
||||
|
||||
- [`docs/birthing/`](../birthing/) — VM birthing plan/status that implements
|
||||
the Tripod contract described in `tripod/TRIPOD.md`.
|
||||
- [`docs/lithosananke/README.md`](../lithosananke/README.md) — kernel-branch
|
||||
overview these designs build on.
|
||||
- [Project root](../../README.md)
|
||||
@@ -1,187 +0,0 @@
|
||||
# ARTEMIS.md — Artemis VM Architecture
|
||||
# StarshipOS / StarForth — Captain Bob (Robert Allan James)
|
||||
# This document constrains Claude Code behavior. Read it completely before touching Artemis.
|
||||
|
||||
---
|
||||
|
||||
## Language Constraint — Non-Negotiable
|
||||
|
||||
All Artemis implementation is in StarForth dialect ONLY.
|
||||
|
||||
This includes:
|
||||
- Data structures
|
||||
- Constants
|
||||
- Variables
|
||||
- Control flow
|
||||
- Everything
|
||||
|
||||
C99 is forbidden unless explicitly blocked in StarForth AND explicit written permission
|
||||
is given by Captain Bob for that specific construct. "I could not figure out how to do
|
||||
this in StarForth" is not permission. Ask first. Wait for the answer.
|
||||
|
||||
If you are about to write a C struct, a #define, or a C variable — stop.
|
||||
Implement it in StarForth or ask.
|
||||
|
||||
---
|
||||
|
||||
## When Stuck — Non-Negotiable
|
||||
|
||||
If you are stuck, STOP.
|
||||
|
||||
Do not confabulate.
|
||||
Do not invent dictionary words that do not exist.
|
||||
Do not fabricate primitives.
|
||||
Do not guess at behavior.
|
||||
Do not work around the problem silently.
|
||||
|
||||
STOP. Report exactly what is blocking you. Wait for instruction.
|
||||
|
||||
Silent confabulation has caused git resets on a project with a hard patent deadline.
|
||||
It is not acceptable under any circumstances.
|
||||
|
||||
---
|
||||
|
||||
## What Artemis Is
|
||||
|
||||
Artemis is memory. She owns the external attached virtual disk image and everything
|
||||
that lives on it. She manages block storage compudynamically.
|
||||
|
||||
Artemis does **not** move messages — that is Hermes.
|
||||
Artemis does **not** make VM lifecycle decisions — that is Hera.
|
||||
Artemis does **not** own the internal ramdisk — that is kernel territory.
|
||||
|
||||
---
|
||||
|
||||
## Storage Topology
|
||||
|
||||
### Internal Ramdisk — Not Artemis Scope
|
||||
- Baked into each VM at build time by mkcapsule.c
|
||||
- LBN 0–3071
|
||||
- Kernel territory
|
||||
- Every VM carries its own ramdisk
|
||||
- Artemis does not touch it, manage it, or know about it
|
||||
|
||||
### External Attached Virtual Disk Image — Artemis Territory
|
||||
- Mounted virtual disk image, attached to the QEMU instance
|
||||
- Artemis owns this exclusively
|
||||
- LBN boundaries to be determined as Artemis is built
|
||||
- Nothing persists between runs yet — that is a future chapter
|
||||
|
||||
### Nothing Persists Between Runs Yet
|
||||
Persistence across runs is a future chapter. Do not implement it yet.
|
||||
Do not design around it. The current model is: VM starts, Artemis initializes
|
||||
her free map, VM stops, everything is gone. That is correct for now.
|
||||
|
||||
---
|
||||
|
||||
## What Artemis Owns
|
||||
|
||||
- The free map over her LBN range on the external disk image
|
||||
- Block fetch and persist operations on the external disk image
|
||||
- ACL lists — structured as Artemis-managed blocks (see ACL section)
|
||||
- Cold capsule store — evicted from Hermes cache (future chapter)
|
||||
- Block metadata
|
||||
|
||||
---
|
||||
|
||||
## Compudynamic Block Lifecycle
|
||||
|
||||
Artemis manages blocks compudynamically. Same model as everything else in StarshipOS:
|
||||
|
||||
- Block enters active use — born hot
|
||||
- Cools over time with each heartbeat tick
|
||||
- Frequently accessed blocks stay warm (heat refreshed on access)
|
||||
- Cold blocks are candidates for eviction or reuse
|
||||
- Block reap must rebalance K correctly
|
||||
|
||||
Artemis is the hardest VM to design because she has three interleaved
|
||||
compudynamic concerns:
|
||||
1. The free map — which LBNs are available
|
||||
2. Block thermal state — how hot is each active block
|
||||
3. K≡1.0 — fleet conservation across all block operations
|
||||
|
||||
These must be designed together. Do not implement one without the others.
|
||||
Do not begin implementation without explicit instruction from Captain Bob.
|
||||
|
||||
---
|
||||
|
||||
## ACL — Access Control Lists
|
||||
|
||||
### Current State
|
||||
ACL is a toggle. It is currently OFF.
|
||||
|
||||
A `\` comment disables ACL enforcement. When commented out, zuse is the
|
||||
implicit and only user. No enforcement occurs.
|
||||
|
||||
```forth
|
||||
\ ACL-ENFORCE ( disabled — zuse only )
|
||||
```
|
||||
|
||||
### Structure
|
||||
ACL lists must be structured as Artemis-managed blocks from day one.
|
||||
Even before Artemis is fully built, ACL data structures must assume
|
||||
they will live in Artemis-managed storage. No shortcuts that require
|
||||
redesign later.
|
||||
|
||||
### When ACL Turns On
|
||||
ACL enforcement becomes mandatory when VMs outside the Tripod arrive.
|
||||
Until then the toggle stays off.
|
||||
|
||||
When enforcement is enabled:
|
||||
- Every VM has an identity
|
||||
- Every operation is checked against the ACL
|
||||
- Artemis is the authority — she holds the lists
|
||||
|
||||
### Security Model
|
||||
Security grows with the threat surface. Not before it.
|
||||
The architecture is always structurally correct — enforcement is simply
|
||||
not active yet. No retrofit needed when the time comes.
|
||||
|
||||
Toggling ACL on must require zero structural changes to the codebase.
|
||||
Only the `\` comment is removed. If toggling ACL requires anything else,
|
||||
the implementation is wrong.
|
||||
|
||||
---
|
||||
|
||||
## What Is Not Artemis
|
||||
|
||||
- **Internal ramdisk** — kernel territory, not Artemis scope
|
||||
- **Message routing** — that is Hermes
|
||||
- **VM lifecycle** — that is Hera
|
||||
- **Persistence across runs** — future chapter, not now
|
||||
- **Cold capsule eviction from Hermes** — future chapter, not now
|
||||
|
||||
---
|
||||
|
||||
## Compudynamic Invariant
|
||||
|
||||
Every block Artemis manages participates in K≡1.0.
|
||||
Block fetch, persist, and reap operations must rebalance K correctly.
|
||||
Artemis's thermal contribution to the fleet is the sum of her active block heat.
|
||||
|
||||
Do not write code that breaks K≡1.0 and add a comment explaining why it's okay.
|
||||
|
||||
---
|
||||
|
||||
## Current Scope
|
||||
|
||||
Artemis is not yet started. Before any implementation begins:
|
||||
|
||||
1. Captain Bob must give explicit instruction to begin
|
||||
2. The three compudynamic concerns (free map, block thermal state, K≡1.0)
|
||||
must be designed together before any code is written
|
||||
3. ACL data structures must be Artemis-block-shaped from first line of code
|
||||
4. Storage boundaries (LBN ranges on external disk image) must be confirmed
|
||||
|
||||
**Do not begin implementation without explicit instruction.**
|
||||
|
||||
Future chapters (do not implement):
|
||||
- Persistence across runs
|
||||
- Cold capsule store from Hermes
|
||||
- Full ACL enforcement
|
||||
- LBN range expansion
|
||||
|
||||
---
|
||||
|
||||
*This document is authoritative. If it conflicts with something in the codebase,
|
||||
the codebase is wrong.*
|
||||
@@ -1,250 +0,0 @@
|
||||
# HERMES.md — Hermes VM Architecture
|
||||
# StarshipOS / StarForth — Captain Bob (Robert Allan James)
|
||||
# This document constrains Claude Code behavior. Read it completely before touching Hermes.
|
||||
|
||||
---
|
||||
|
||||
## Language Constraint — Non-Negotiable
|
||||
|
||||
All Hermes implementation is in StarForth dialect ONLY.
|
||||
|
||||
This includes:
|
||||
- Data structures
|
||||
- Constants
|
||||
- Variables
|
||||
- Control flow
|
||||
- Everything
|
||||
|
||||
C99 is forbidden unless explicitly blocked in StarForth AND explicit written permission
|
||||
is given by Captain Bob for that specific construct. "I could not figure out how to do
|
||||
this in StarForth" is not permission. Ask first. Wait for the answer.
|
||||
|
||||
If you are about to write a C struct, a #define, or a C variable — stop.
|
||||
Implement it in StarForth or ask.
|
||||
|
||||
---
|
||||
|
||||
## What Hermes Is
|
||||
|
||||
Hermes is the messenger. He moves messages between VMs and manages channels.
|
||||
That is his complete contract.
|
||||
|
||||
Hermes does **not** store persistent data — that is Artemis.
|
||||
Hermes does **not** make lifecycle decisions — that is Hera.
|
||||
Hermes does **not** route by load or heat — dispatch is capability-based, always.
|
||||
|
||||
Capsules are baked into the OS blob by mkcapsule.c at build time.
|
||||
Hermes has no capsule cache, no fetch logic, no repository concern.
|
||||
That is a future chapter.
|
||||
|
||||
---
|
||||
|
||||
## The Event Loop
|
||||
|
||||
Hermes runs a compudynamic event loop. Every message is a compudynamic object:
|
||||
|
||||
- Born hot (full heat at creation)
|
||||
- Cools each heartbeat tick
|
||||
- ACK received → clean death, K redistributed to fleet
|
||||
- NACK received → requeue with reduced heat, or reaped if heat floor reached
|
||||
- TTL expires (heat → 0) → Hermes reaps the message, K rebalanced
|
||||
|
||||
There is no special timeout logic. The physics handles it.
|
||||
A message that nobody answers simply cools to death.
|
||||
|
||||
---
|
||||
|
||||
## Message Structure
|
||||
|
||||
Every message carries:
|
||||
|
||||
```
|
||||
type — work type tag (determines recipient)
|
||||
sender — originating VM identity
|
||||
recipient — destination VM identity
|
||||
payload — message body
|
||||
heat — current thermal value (compudynamic)
|
||||
sequence — monotonic sequence number
|
||||
```
|
||||
|
||||
Point-to-point only. Sender addresses recipient directly.
|
||||
Hermes delivers and tracks thermal state. He does not inspect payload.
|
||||
|
||||
---
|
||||
|
||||
## ACK/NACK Protocol
|
||||
|
||||
- ACK → message dies cleanly, K redistributed
|
||||
- NACK → message requeued with reduced heat
|
||||
- No response → message cools naturally to death via TTL
|
||||
|
||||
The binary receipt of a response IS the ACK where applicable.
|
||||
No separate acknowledgement frame needed in those cases.
|
||||
|
||||
---
|
||||
|
||||
## PubSub — Channels
|
||||
|
||||
Hermes implements a publish/subscribe model. Topics are called **channels**.
|
||||
|
||||
### The Common Channel
|
||||
|
||||
There is one permanent channel: `COMMON`.
|
||||
|
||||
- Always exists, always hot
|
||||
- Any VM can publish to it
|
||||
- Used for negotiation and channel establishment only
|
||||
- Not for business transactions — those happen on ephemeral channels
|
||||
|
||||
### Ephemeral Channels
|
||||
|
||||
Ephemeral channels are compudynamic objects — born hot, reaped when cold or closed.
|
||||
|
||||
**Channel structure:**
|
||||
|
||||
```
|
||||
channel_id — owner VM identity + monotonic sequence number
|
||||
owner — VM that created the channel (always the responder)
|
||||
members[] — participant list
|
||||
heat — compudynamic, born hot at creation
|
||||
state — NEGOTIATING | OPEN | CLOSING
|
||||
```
|
||||
|
||||
### The Negotiation Protocol
|
||||
|
||||
```
|
||||
1. X publishes request on COMMON — born hot, TTL ticking
|
||||
2. Y sees request, responds yes/no on COMMON
|
||||
— No response → message cools to death → implicit NACK to X
|
||||
3. Y accepts → Y creates ephemeral channel
|
||||
→ Y publishes channel_id to X over COMMON
|
||||
4. X and Y conduct business on ephemeral channel
|
||||
5. Business concluded → owner Y reaps channel → K rebalanced
|
||||
```
|
||||
|
||||
Y owns channel creation and destruction. Always the responder, never the requester.
|
||||
A channel dying of cold (abandoned transaction) is not an error — the physics handles it.
|
||||
|
||||
### Multi-Party Channels
|
||||
|
||||
Channels are bilateral by default. The owner may invite additional VMs:
|
||||
|
||||
```
|
||||
1. Owner publishes invite to candidate VM on COMMON
|
||||
2. Candidate accepts or declines on COMMON — same TTL/cool protocol
|
||||
3. Accept → candidate added to members[]
|
||||
4. Decline or timeout → candidate never joins, channel continues bilateral
|
||||
```
|
||||
|
||||
Multi-party is designed for but not implemented yet.
|
||||
Do not implement invite logic until explicitly instructed.
|
||||
The members[] structure must exist from the start to avoid future redesign.
|
||||
|
||||
### Channel Identity
|
||||
|
||||
`channel_id` = owner VM identity + monotonic sequence number.
|
||||
Unforgeable by non-owners. Hermes mints it. No VM constructs its own channel_id.
|
||||
|
||||
### Compudynamic Invariant for Channels
|
||||
|
||||
Channels participate in K≡1.0.
|
||||
An open channel with active messages holds heat.
|
||||
Channel reap must redistribute K correctly to the fleet.
|
||||
A channel cannot be reaped while messages on it are still in flight —
|
||||
drain first, then reap.
|
||||
|
||||
---
|
||||
|
||||
## What Is Not Hermes
|
||||
|
||||
- **Capsule cache** — future chapter, not now
|
||||
- **Remote fetch** — future chapter, not now
|
||||
- **UDP server / client** — future chapter, not now
|
||||
- **Instance authentication** — future chapter, not now
|
||||
- **Persistent block storage** — that is Artemis
|
||||
- **VM lifecycle decisions** — that is Hera
|
||||
- **Heat-based routing** — wrong model, never implement
|
||||
|
||||
---
|
||||
|
||||
## Compudynamic Invariant
|
||||
|
||||
Every object Hermes manages — messages and channels — participates in K≡1.0.
|
||||
Fleet K includes the thermal contribution of in-flight messages and open channels.
|
||||
Hermes reaping a message or channel must rebalance K correctly.
|
||||
|
||||
Do not write code that breaks K≡1.0 and add a comment explaining why it's okay.
|
||||
|
||||
---
|
||||
|
||||
## Current Scope
|
||||
|
||||
1. Compudynamic event loop — message emit, drain, TTL, ACK/NACK, reap
|
||||
2. COMMON channel — permanent, always hot, negotiation only
|
||||
3. Ephemeral channels — compudynamic lifecycle, owner=responder, bilateral default
|
||||
4. Channel negotiation protocol — request on COMMON, Y creates, Y reaps
|
||||
5. members[] structure — present from the start, multi-party invite not yet implemented
|
||||
|
||||
Capsule management is a future chapter.
|
||||
Remote repository is a future chapter.
|
||||
Multi-party channel invite is a future chapter.
|
||||
|
||||
---
|
||||
|
||||
## v1 Block Map — LOCKED
|
||||
|
||||
Blocks 4110–4113 are Artemis. NEVER touch them.
|
||||
|
||||
```
|
||||
4100 Constants: event codes, channel states, node sizes, arena sizes
|
||||
4101 Arena CREATE: MSG-ARENA CH-ARENA MBR-ARENA; free-list vars; MSG-SEQ CH-ACTIVE
|
||||
4102 MSG-INIT-FREE + CH-INIT-FREE
|
||||
4103 MBR-INIT-FREE + MSG-ALLOC + MSG-FREE-NODE
|
||||
4104 CH-ALLOC + CH-FREE-NODE + MBR-ALLOC + MBR-FREE-NODE
|
||||
4105 Message field accessors: MSG-TYPE@/! MSG-FROM@/! MSG-TO@/! MSG-PADDR@/! MSG-PLEN@/! MSG-HEAT@/! MSG-SEQ@/!
|
||||
4106 Channel+member accessors: CH-ID@/! CH-OWNER@/! CH-STATE@/! CH-HEAT@/! CH-MBRS@/! CH-NEXT@/! MBR-NEXT@ MBR-VM@
|
||||
4107 IDX>NAME + MSG-DELIVER + MSG-SEND
|
||||
4108 VARIABLE MSG-SCAN + MSG-COOL-ONE + MSG-COOL-ALL
|
||||
4109 MSG-REAP
|
||||
---- 4110–4113: ARTEMIS — DO NOT TOUCH ----
|
||||
4114 VARIABLE CH-SCAN + CH-COOL-ALL
|
||||
4115 CH-REAP-SAFE
|
||||
4116 VARIABLE COMMON-CH + COMMON-INIT + HERMES-TICK
|
||||
4117 EVENT-EMIT + EVENT-WAIT + EVENT-DRAIN (backward compat)
|
||||
4118 HERA-NOTIFY-SPAWN + HERA-NOTIFY-KILL + HERA-DISPATCH-ONE + HERA-DISPATCH
|
||||
4119 CH-REQUEST + CH-ACCEPT + CH-CLOSE
|
||||
4120 WELCOME + CD-INIT
|
||||
```
|
||||
|
||||
### Node layouts (cells)
|
||||
|
||||
**Message node — 7 cells:**
|
||||
- 0: type (in-use) / next-free ptr (free)
|
||||
- 1: sender VM index
|
||||
- 2: recipient VM index
|
||||
- 3: payload addr (FORTH string addr)
|
||||
- 4: payload len
|
||||
- 5: heat (Q48.16)
|
||||
- 6: seq
|
||||
|
||||
**Channel node — 6 cells:**
|
||||
- 0: channel-id (in-use) / next-free ptr (free)
|
||||
- 1: owner VM index
|
||||
- 2: state (0=NEGOTIATING 1=OPEN 2=CLOSING)
|
||||
- 3: heat (Q48.16)
|
||||
- 4: members-head (→ member list)
|
||||
- 5: next-active (active channel list link)
|
||||
|
||||
**Member node — 2 cells:**
|
||||
- 0: next-ptr
|
||||
- 1: vm-id
|
||||
|
||||
### Physics
|
||||
|
||||
Cooling constant: Q-DECAY (65208) from compudynamics.4th — same as VM-DECAY-ONE.
|
||||
Messages and VMs cool at identical rates. Fleet is thermodynamically consistent.
|
||||
|
||||
---
|
||||
|
||||
*This document is authoritative. If it conflicts with something in the codebase,
|
||||
the codebase is wrong.*
|
||||
@@ -1,28 +0,0 @@
|
||||
# docs/03-architecture/tripod/
|
||||
|
||||
Architectural constraints for the three StarForth VMs that make up the
|
||||
Tripod. These documents are binding — read the relevant one in full before
|
||||
touching any Tripod code. Violating the mythological contract they describe
|
||||
is treated as an architectural error, not a style preference.
|
||||
|
||||
- **[TRIPOD.md](TRIPOD.md)** — The Tripod as a whole: Hera (VM-HERA=0,
|
||||
governor — spawns/manages/reaps VMs), Hermes (VM-HERMES=1, messenger —
|
||||
moves events), Artemis (VM-ARTEMIS=2, memory — owns block storage).
|
||||
Covers capability-based dispatch (no heat-based routing), the CD-TICK
|
||||
heartbeat, the K≡1.0 compudynamic conservation invariant, the DoE test
|
||||
fixture's role, and explicit prohibitions (no heat-based VM routing, no
|
||||
primitives added without instruction, no `BLOCK` calls outside the
|
||||
0–3071 ramdrive range).
|
||||
- **[HERMES.md](HERMES.md)** — Hermes VM architecture: the messenger role.
|
||||
- **[ARTEMIS.md](ARTEMIS.md)** — Artemis VM architecture: the memory/block-
|
||||
storage role.
|
||||
|
||||
All three documents share a non-negotiable constraint: Tripod implementation
|
||||
is StarForth dialect only — no C99 without Captain Bob's explicit written
|
||||
permission for that specific construct.
|
||||
|
||||
## See also
|
||||
|
||||
- [`docs/birthing/`](../../birthing/) — birthing plan and QEMU acceptance
|
||||
logs for the Hera-spawns-Hermes/Artemis constellation described here.
|
||||
- [Project root](../../../README.md)
|
||||
@@ -1,188 +0,0 @@
|
||||
# TRIPOD.md — Architectural Constraints for the Tripod VMs
|
||||
# StarshipOS / StarForth — Captain Bob (Robert Allan James)
|
||||
# This document constrains Claude Code behavior. Read it completely before touching any Tripod code.
|
||||
|
||||
---
|
||||
|
||||
## The Tripod: What It Is
|
||||
|
||||
Three StarForth VMs constitute the Tripod. They are not generic workers. Each holds a
|
||||
specific architectural contract expressed by its mythological name. Violating the
|
||||
mythological contract is an architectural error, not a style preference.
|
||||
|
||||
| VM | ID | Contract |
|
||||
|------------|-------------|-----------------------------------------------|
|
||||
| Hera | VM-HERA=0 | Governor. Spawns, manages, and reaps VMs. |
|
||||
| Hermes | VM-HERMES=1 | Messenger. Moves events between VMs. |
|
||||
| Artemis | VM-ARTEMIS=2| Memory. Owns block storage and persistence. |
|
||||
|
||||
**Hera is queen. She does not do work. She governs who exists and who doesn't.**
|
||||
**Hermes moves messages. He does not store anything.**
|
||||
**Artemis holds things. She does not route anything.**
|
||||
|
||||
If you find yourself putting event dispatch logic in Artemis, or storage logic in Hermes,
|
||||
or work execution logic in Hera — stop. You have the wrong VM.
|
||||
|
||||
---
|
||||
|
||||
## The Immediate Goal
|
||||
|
||||
Hera must spawn Hermes and Artemis at boot, and all three must cooperate
|
||||
compudynamically under K≡1.0 conservation.
|
||||
|
||||
That is the complete scope. Nothing else.
|
||||
|
||||
Acceptance criteria:
|
||||
1. Hera boots and initializes her own compudynamic state.
|
||||
2. Hera spawns Hermes. Hermes initializes his own compudynamic state.
|
||||
3. Hera spawns Artemis. Artemis initializes her own compudynamic state.
|
||||
4. All three VMs are running. Fleet K = sum of individual VM K values. K≡1.0 holds.
|
||||
5. Hera can reap (cleanly terminate) a child VM.
|
||||
6. The system is stable across a long-running test workload.
|
||||
|
||||
---
|
||||
|
||||
## Compudynamics: Dual Role — Read This Carefully
|
||||
|
||||
Compudynamics serves TWO roles in this system. Do not conflate them.
|
||||
|
||||
### Role 1: Intra-VM Physics Engine
|
||||
Inside each VM, Compudynamics drives the adaptive heartbeat:
|
||||
- 7-loop rolling window
|
||||
- K conservation arithmetic
|
||||
- Phase operators on the heartbeat signal
|
||||
|
||||
Every VM — Hera, Hermes, Artemis — runs its own compudynamic engine internally.
|
||||
This is autonomous. No VM manages another VM's internal heartbeat.
|
||||
|
||||
### Role 2: Hera's VM Lifecycle Driver
|
||||
Hera observes the fleet K picture and uses it to make **lifecycle decisions**:
|
||||
- Is a child VM healthy?
|
||||
- Is a child VM starved?
|
||||
- Does a child VM need to be spawned, suspended, or reaped?
|
||||
|
||||
Hera does NOT use fleet K to route work. She uses it to govern existence.
|
||||
|
||||
**The fleet K view is lifecycle telemetry. It is not a dispatch mechanism.**
|
||||
|
||||
---
|
||||
|
||||
## Dispatch: Capability-Based, Always
|
||||
|
||||
Work routing is determined by work type. It is not determined by heat, K value,
|
||||
VM load, or any compudynamic signal.
|
||||
|
||||
| Work type | Destination |
|
||||
|-----------------|-------------|
|
||||
| Block I/O | Artemis |
|
||||
| Event emit/drain| Hermes |
|
||||
| VM lifecycle | Hera |
|
||||
|
||||
`VM-EXEC` takes a VM name. The caller names the correct VM for the work type.
|
||||
There is no routing algorithm. There is no dispatch table keyed on heat.
|
||||
There is no "send to the hottest VM." That model is wrong and must not be implemented.
|
||||
|
||||
---
|
||||
|
||||
## CD-TICK: What It Is and Is Not
|
||||
|
||||
CD-TICK advances the compudynamic heartbeat. That is all it does.
|
||||
|
||||
CD-TICK is **not**:
|
||||
- A scheduler
|
||||
- A timeslicer
|
||||
- A run-queue manager
|
||||
- A work dispatcher
|
||||
- A router
|
||||
|
||||
If you are calling CD-TICK to decide where work goes, you are using it wrong.
|
||||
|
||||
---
|
||||
|
||||
## The DoE (Design of Experiments) Test Fixture
|
||||
|
||||
The DoE campaign (PHASE6-TEST, K-conservation CSV logging, 38,400-run Latin Square)
|
||||
is a **stress and measurement fixture**. It exists to:
|
||||
- Validate K≡1.0 conservation under long-running diverse workloads
|
||||
- Generate telemetry for the SSRN paper
|
||||
- Provide a long-runtime acceptance test for the compudynamic physics
|
||||
|
||||
The DoE is **not**:
|
||||
- A description of what the system does in production
|
||||
- A feature
|
||||
- A model for how work gets dispatched
|
||||
|
||||
`DOE-WORK` must never appear in the production dispatch path.
|
||||
If you see `DOE-WORK` being dispatched by anything other than the test fixture, remove it.
|
||||
|
||||
The DoE is a good test precisely because it is long-running and diverse.
|
||||
It exercises the physics. It does not define the system.
|
||||
|
||||
---
|
||||
|
||||
## What Not To Do — Explicit Prohibitions
|
||||
|
||||
1. **Do not implement heat-based VM routing.** It causes starvation. It is wrong.
|
||||
2. **Do not pin Hera's heat floor.** That is a band-aid on a wrong model.
|
||||
3. **Do not put DOE-WORK in the production dispatch path.**
|
||||
4. **Do not call CD-TICK a scheduler** in comments, docs, or variable names.
|
||||
5. **Do not call the fleet K view a router** in comments, docs, or variable names.
|
||||
6. **Do not add primitives to StarForth without explicit instruction.**
|
||||
NIP is not registered. TUCK is not registered. Assume nothing is available
|
||||
that is not in the verified primitive table. Use SWAP DROP instead of NIP.
|
||||
7. **Do not call BLOCK on LBNs outside the ramdrive range (0–3071).**
|
||||
LBN 4501–4599 are Artemis metadata space. They are not in the kernel ramdrive.
|
||||
Use ART-STATUS to touch the free map. Do not call ART-SELF-TEST in acceptance tests.
|
||||
8. **Do not exceed 64 bytes per line or 16 lines per block in capsule files.**
|
||||
mkcapsule.c enforces this at build time. Violations will fail the build.
|
||||
|
||||
---
|
||||
|
||||
## The Invariant
|
||||
|
||||
K≡1.0 is conserved across the fleet at all times.
|
||||
Fleet K = sum of all VM K values.
|
||||
This is a physics constraint, not a software convention.
|
||||
Do not write code that breaks it and then add a comment explaining why it's okay.
|
||||
|
||||
---
|
||||
|
||||
*This document is authoritative. If it conflicts with something in the codebase,
|
||||
the codebase is wrong.*
|
||||
|
||||
---
|
||||
|
||||
## Language Constraint — Non-Negotiable
|
||||
|
||||
All Tripod implementation is in StarForth dialect ONLY.
|
||||
|
||||
This includes:
|
||||
- Data structures
|
||||
- Constants
|
||||
- Variables
|
||||
- Control flow
|
||||
- Everything
|
||||
|
||||
C99 is forbidden unless explicitly blocked in StarForth AND explicit written permission
|
||||
is given by Captain Bob for that specific construct. "I could not figure out how to do
|
||||
this in StarForth" is not permission. Ask first. Wait for the answer.
|
||||
|
||||
If you are about to write a C struct, a #define, or a C variable — stop.
|
||||
Implement it in StarForth or ask.
|
||||
|
||||
---
|
||||
|
||||
## When Stuck — Non-Negotiable
|
||||
|
||||
If you are stuck, STOP.
|
||||
|
||||
Do not confabulate.
|
||||
Do not invent dictionary words that do not exist.
|
||||
Do not fabricate primitives.
|
||||
Do not guess at behavior.
|
||||
Do not work around the problem silently.
|
||||
|
||||
STOP. Report exactly what is blocking you. Wait for instruction.
|
||||
|
||||
Silent confabulation has caused git resets on a project with a hard patent deadline.
|
||||
It is not acceptable under any circumstances.
|
||||
@@ -1,404 +0,0 @@
|
||||
# Word-Level ACL System
|
||||
|
||||
**Status:** Implemented through Phase 7 (LithosAnanke kernel parity) — independently verified
|
||||
present in current `master` (`.claude/CLAUDE.md`'s Word-Level ACL System section). Phase 8
|
||||
(PKI/thumbdrive minting) is the current open item.
|
||||
**Target branch:** `master` — post-split, this repo's sole production line; there is no
|
||||
separate `lithosananke` branch to reach parity with (see `.claude/CLAUDE.md`'s "On the branch
|
||||
topology" note)
|
||||
**Implementation files:** `capsules/ACL.4th`, `capsules/zuse.4th`, `src/word_source/acl_words.c`, `src/test_runner/modules/acl_words_test.c`
|
||||
|
||||
---
|
||||
|
||||
## Summary
|
||||
|
||||
### Overview
|
||||
|
||||
A word-level access control system for StarForth VMs, implemented as a
|
||||
combination of a thin C infrastructure layer and a pure-FORTH policy capsule
|
||||
(`ACL.4th`). The C layer provides four `DictEntry` fields for the hot path
|
||||
(TTL counter + allow bit + mode + pin). All policy, all adaptive logic, all
|
||||
inheritance rules live as colon definitions in `ACL.4th`. A bootstrap
|
||||
superuser (`zuse.4th`) provides the sole authenticated escalation path.
|
||||
|
||||
---
|
||||
|
||||
### ACL Disposition — Three States
|
||||
|
||||
Each word in the dictionary has one of three enforcement dispositions:
|
||||
|
||||
| State | Behavior |
|
||||
|-------|---------|
|
||||
| `STRICT` | ACL re-checked on every execution |
|
||||
| `TTL` | ACL cached; re-checked only when TTL counter reaches zero |
|
||||
| `PINNED` | Current mode and decision frozen permanently; one-way ratchet |
|
||||
|
||||
---
|
||||
|
||||
### TTL — Statistically Adaptive
|
||||
|
||||
The TTL is not a fixed value. It is derived and continuously updated from
|
||||
the existing SSM execution physics:
|
||||
|
||||
- **Heat** (`execution_heat`): hotter words earn longer TTLs; check cost
|
||||
amortized over more executions
|
||||
- **Rolling window**: sudden shift in caller pattern or access rate causes
|
||||
TTL to shrink aggressively
|
||||
- **Decay**: quiescent words pull their TTL back down so the next burst
|
||||
re-validates early
|
||||
- **Inference engine** (L5/L6): detects oscillating TTL and stabilizes it —
|
||||
same CV threshold logic already used for window-width inference
|
||||
|
||||
`PINNED` is the asymptote: the adaptive process converges, you thumbtack
|
||||
it, and the accumulator freezes permanently.
|
||||
|
||||
A FORTH security word selects enforcement mode per word:
|
||||
|
||||
```forth
|
||||
' MY-WORD ACL-STRICT \ check every execution
|
||||
' MY-WORD ACL-TTL-MODE \ use adaptive TTL
|
||||
' MY-WORD ACL-PIN \ freeze — mode and decision immutable forever
|
||||
```
|
||||
|
||||
---
|
||||
|
||||
### The Thumbtack / Pin Flag
|
||||
|
||||
`ACL-PIN ( xt -- )` is a one-way ratchet:
|
||||
|
||||
- Transitions: `STRICT → PINNED` or `TTL → PINNED` — never back
|
||||
- Once pinned, `acl_mode` and `acl_ttl` are immutable for that VM context
|
||||
- Any attempt to change a pinned word's ACL is silently ignored (or errors,
|
||||
depending on policy)
|
||||
- Kernel primitive words (`BIRTH`, `EXEC`, `BYE`, etc.) are pinned by Mama
|
||||
at boot before the first `BIRTH` fires
|
||||
|
||||
---
|
||||
|
||||
### Inheritance at Birth
|
||||
|
||||
When a child VM is born:
|
||||
|
||||
```
|
||||
acl_mode = parent->acl_mode \ policy propagates (STRICT or TTL)
|
||||
acl_pinned = 0 \ always clear — child owns its own lock
|
||||
acl_ttl = default \ reset; child has no execution history
|
||||
acl_decision = ALLOW \ re-evaluated on first access
|
||||
```
|
||||
|
||||
Key properties:
|
||||
|
||||
- **Pin is contextual, not viral.** A parent's pinned words do not force
|
||||
the child to be pinned. The child inherits the mode as a starting point
|
||||
and can tighten, relax, or re-pin freely.
|
||||
- **Security lattice flows downward at birth only.** After birth, each VM's
|
||||
ACL state is independent. A compromised child cannot bootstrap its way
|
||||
back to Mama's pinned ACLs.
|
||||
|
||||
---
|
||||
|
||||
### Interpreter Hook — Two-Level Check
|
||||
|
||||
The C interpreter reads only two fields per `DictEntry`:
|
||||
|
||||
```c
|
||||
if (vm->emergency_console) goto execute; /* 100% bypass — physical access */
|
||||
if (entry->acl_ttl-- > 0) goto execute; /* TTL good — single decrement */
|
||||
acl_recheck(vm, entry); /* TTL=0: call FORTH ACL-RECHECK */
|
||||
if (!entry->acl_allow) goto reject;
|
||||
```
|
||||
|
||||
**Hot path cost:** one decrement and a branch — essentially free.
|
||||
**Cold path:** calls `ACL-RECHECK` in `ACL.4th`, which recomputes the
|
||||
adaptive TTL, updates `acl_allow`, and resets the counter. The C side
|
||||
never reasons about policy; it only reads the result.
|
||||
|
||||
---
|
||||
|
||||
### Two-Console Architecture
|
||||
|
||||
Two permanent, independent console layers exist at all times:
|
||||
|
||||
#### 1. Emergency Console (always present)
|
||||
|
||||
- `emergency_console` (`uint8_t`) flag in `VM` struct — C-only write; no
|
||||
FORTH word sets it
|
||||
- Checked first in the interpreter hot path — 100% ACL bypass
|
||||
- `acl_recheck()` uses save/restore around it for re-entrancy protection
|
||||
- `EMERGENCY_CONSOLE_ENABLED` Makefile build flag (default=1): when set to
|
||||
0, strips interactive fallthrough; `vm_fault_handler()` weak symbol is
|
||||
called instead (override for hardware reset, watchdog, debug probe)
|
||||
- `BYE` returns to the emergency console
|
||||
- Only `panic` kills the VM
|
||||
- Prompt: `ok>`
|
||||
|
||||
#### 2. Zuse Console (omnipresent, awaiting authentication)
|
||||
|
||||
- `zuse_session` (`uint8_t`) flag in `VM` struct — C-only write; no FORTH
|
||||
word sets it
|
||||
- Prompt: `zuse)ok>`
|
||||
- Full ACL bypass when a Zuse session is active
|
||||
- Completely independent of `emergency_console` — setting one does not
|
||||
affect the other
|
||||
|
||||
---
|
||||
|
||||
### Superuser: Zuse
|
||||
|
||||
Named for Konrad Zuse, pioneer of programmable computers. Zuse is the
|
||||
bootstrap superuser: the sole entity that can own the zuse console and mint
|
||||
user credentials.
|
||||
|
||||
- Defined in `capsules/zuse.4th`, loaded by `ACL.4th` at capsule boot
|
||||
- Software-only for now (no thumbdrive); `zuse.4th` is a capsule citizen
|
||||
from day one
|
||||
- Zuse's words are pinned by `ACL-ZUSE-BOOT` at load time
|
||||
- `ACL-BOOT` is called first, then `S" zuse.4th" EXEC` — both from within
|
||||
`ACL.4th` itself (Block 2067)
|
||||
- Future: replace with thumbdrive PKI (Ed25519 challenge-response);
|
||||
`zuse.4th` becomes the bootstrapper that validates the physical drive
|
||||
|
||||
---
|
||||
|
||||
### CA Root
|
||||
|
||||
- Embedded in `ACL.4th` (Block 2066) as constants `ACL-CA-KEY-LO` /
|
||||
`ACL-CA-KEY-HI`
|
||||
- Capsule hash = root-of-trust fingerprint: any CA key change changes the
|
||||
capsule hash and the birth protocol detects tampering
|
||||
- Placeholder (zeros) until `tools/mkcapsule` embeds the real Ed25519 key
|
||||
at build time
|
||||
|
||||
---
|
||||
|
||||
### Security Model / No-Security Condition
|
||||
|
||||
Security is opt-in via `init.4th`. The toggle is one commented-out line:
|
||||
|
||||
```forth
|
||||
\ S" ACL.4th" EXEC
|
||||
```
|
||||
|
||||
| `ACL.4th` | `zuse.4th` | Result |
|
||||
|-----------|------------|--------|
|
||||
| absent | absent | No security — open dev mode |
|
||||
| present | absent | ACL enforced; emergency REPL locked until Zuse provisioned |
|
||||
| present | present | Full lockdown; Zuse owns the zuse console |
|
||||
|
||||
Uncomment the line in `init.4th` to enable full lockdown. Leave it
|
||||
commented out for development builds.
|
||||
|
||||
---
|
||||
|
||||
### Self-Activating Capsule
|
||||
|
||||
`ACL.4th` is self-activating — `init.4th` only needs one line:
|
||||
|
||||
```forth
|
||||
S" ACL.4th" EXEC
|
||||
```
|
||||
|
||||
Internal structure of `ACL.4th`:
|
||||
- **Block 2066**: CA root placeholder constants (`ACL-CA-KEY-LO` /
|
||||
`ACL-CA-KEY-HI`)
|
||||
- **Block 2067**: Calls `ACL-BOOT` then `S" zuse.4th" EXEC`
|
||||
|
||||
`ACL-BOOT` stamps default ACL entries on all existing dictionary words.
|
||||
After it runs, every subsequent `:` definition gets an ACL entry via the
|
||||
defining-word hook. No word can exist without an ACL entry.
|
||||
|
||||
---
|
||||
|
||||
### Emergency Console — 100% Bypass
|
||||
|
||||
`vm->emergency_console` is set by the C layer when the physical `ok>` REPL
|
||||
is active. It is checked first, before any ACL table lookup. Physical
|
||||
presence always wins. The emergency console is never subject to ACL
|
||||
constraints regardless of what `ACL.4th` defines.
|
||||
|
||||
The `EMERGENCY_CONSOLE_ENABLED=0` build flag strips the interactive
|
||||
fallthrough for production or embedded builds, routing faults to
|
||||
`vm_fault_handler()` instead.
|
||||
|
||||
---
|
||||
|
||||
### ACL.4th — Pure FORTH Implementation
|
||||
|
||||
The ACL table is a `CREATE`d FORTH array indexed by execution token (XT).
|
||||
`'` (tick) gives the XT of any word; XT is just a cell value usable as a
|
||||
table key.
|
||||
|
||||
Core words:
|
||||
|
||||
| Word | Stack | Description |
|
||||
|------|-------|-------------|
|
||||
| `ACL-ENTRY` | `( xt -- addr )` | O(1) table lookup by XT |
|
||||
| `ACL-MODE@` | `( xt -- mode )` | read enforcement mode |
|
||||
| `ACL-MODE!` | `( mode xt -- )` | set mode (no-op if pinned) |
|
||||
| `ACL-PINNED?` | `( xt -- flag )` | test pin bit |
|
||||
| `ACL-PIN` | `( xt -- )` | set pin — one-way, irreversible |
|
||||
| `ACL-STRICT` | `( xt -- )` | set STRICT mode (no-op if pinned) |
|
||||
| `ACL-TTL-MODE` | `( xt -- )` | set TTL mode (no-op if pinned) |
|
||||
| `ACL-TTL@` | `( xt -- n )` | read current TTL counter |
|
||||
| `ACL-TTL!` | `( n xt -- )` | write TTL counter |
|
||||
| `ACL-ALLOW@` | `( xt -- flag )` | read cached allow/deny decision |
|
||||
| `ACL-ALLOW!` | `( flag xt -- )` | write allow/deny decision |
|
||||
| `ACL-INHERIT` | `( src dst -- )` | birth inheritance: copy mode, clear pin, reset ttl+decision |
|
||||
| `ACL-RECHECK` | `( xt -- )` | adaptive TTL recomputation; updates allow + new TTL |
|
||||
| `ACL-INIT-PRIMITIVES` | `( -- )` | bulk-initialize ACL entries for all existing dictionary words |
|
||||
|
||||
Example pin at boot in `init.4th`:
|
||||
|
||||
```forth
|
||||
' BIRTH ACL-STRICT ' BIRTH ACL-PIN
|
||||
' EXEC ACL-STRICT ' EXEC ACL-PIN
|
||||
' BYE ACL-STRICT ' BYE ACL-PIN
|
||||
```
|
||||
|
||||
---
|
||||
|
||||
### Bootstrap Sequence
|
||||
|
||||
```forth
|
||||
\ In init.4th (one line, opt-in toggle — uncomment to enable):
|
||||
S" ACL.4th" EXEC \ self-activating: calls ACL-BOOT then loads zuse.4th
|
||||
|
||||
\ ACL.4th Block 2067 does internally:
|
||||
ACL-BOOT \ stamp default ACLs on all existing words
|
||||
S" zuse.4th" EXEC \ load and pin Zuse's words
|
||||
|
||||
\ Subsequent capsule loads (e.g. doe.4th) get ACL entries via : hook
|
||||
S" doe.4th" EXEC
|
||||
```
|
||||
|
||||
Every `:` definition after `ACL-BOOT` runs creates its own ACL entry at
|
||||
definition time via a hook in the defining word. No word is ever born
|
||||
without an ACL entry.
|
||||
|
||||
---
|
||||
|
||||
### Capsule Namespace
|
||||
|
||||
| File | Role |
|
||||
|------|------|
|
||||
| `init.4th` | Mama VM personality (default); contains opt-in ACL toggle |
|
||||
| `init-*.4th` | Alternate personalities |
|
||||
| `doe.4th` | DoE experiment harness |
|
||||
| `ACL.4th` | Word-level ACL subsystem — self-activating; loads `zuse.4th` |
|
||||
| `zuse.4th` | Bootstrap superuser personality; words pinned by `ACL-ZUSE-BOOT` |
|
||||
| `std-blob.4th` | Standard library layer (future) |
|
||||
|
||||
---
|
||||
|
||||
## Implementation Punch List
|
||||
|
||||
### Phase 1 — C Infrastructure (`master`) ✅ COMPLETE
|
||||
|
||||
- [x] Add `acl_ttl` (`uint32_t`) to `DictEntry` in `include/vm.h`
|
||||
- [x] Add `acl_allow` (`uint8_t`) to `DictEntry`
|
||||
- [x] Add `acl_mode` (`uint8_t`: STRICT=0 / TTL=1) to `DictEntry`
|
||||
- [x] Add `acl_pinned` (`uint8_t`) to `DictEntry`
|
||||
- [x] Default-initialize all four fields in `word_register()`:
|
||||
`ttl=ACL_OPEN, allow=1, mode=TTL, pinned=0`
|
||||
- [x] Add `emergency_console` (`uint8_t`) flag to `VM` struct
|
||||
- [x] Add `zuse_session` (`uint8_t`) flag to `VM` struct
|
||||
- [x] Insert two-level ACL check into interpreter loop in `vm.c`
|
||||
- [x] Implement `acl_recheck()` in `vm.c` — calls FORTH `ACL-RECHECK` when
|
||||
TTL=0; save/restore `emergency_console` for re-entrancy protection
|
||||
- [x] Add `:` definition hook to create ACL entry for each newly defined word
|
||||
|
||||
### Phase 2 — C Primitive Words + `ACL.4th` Capsule (`master`) ✅ COMPLETE
|
||||
|
||||
- [x] 12 C primitive words in `src/word_source/acl_words.c`
|
||||
- [x] `CREATE ACL-TABLE` sized to max dictionary entries
|
||||
- [x] `ACL-ENTRY ( xt -- addr )` — XT-indexed O(1) lookup
|
||||
- [x] Field accessors: `ACL-MODE@`, `ACL-MODE!`, `ACL-PINNED?`,
|
||||
`ACL-TTL@`, `ACL-TTL!`, `ACL-ALLOW@`, `ACL-ALLOW!`
|
||||
- [x] `ACL-PIN ( xt -- )` — one-way ratchet; no-op if already pinned
|
||||
- [x] `ACL-STRICT ( xt -- )` — set STRICT mode; no-op if pinned
|
||||
- [x] `ACL-TTL-MODE ( xt -- )` — set TTL mode; no-op if pinned
|
||||
- [x] `ACL-INHERIT ( src-xt dst-xt -- )` — copy mode, clear pin,
|
||||
reset ttl+decision
|
||||
- [x] `ACL-RECHECK ( xt -- )` — recompute adaptive TTL from heat and rolling
|
||||
window; update `acl_allow` and reset counter
|
||||
- [x] `ACL-INIT-PRIMITIVES` — walk dictionary, create default entry per word
|
||||
- [x] Pin privileged words: `BIRTH`, `EXEC`, `BYE`, and other Mama-only words
|
||||
|
||||
### Phase 3 — `capsules/ACL.4th` Self-Activating Capsule (`master`) ✅ COMPLETE
|
||||
|
||||
- [x] `ACL.4th` is self-activating: Block 2067 calls `ACL-BOOT` then
|
||||
`S" zuse.4th" EXEC`
|
||||
- [x] Block 2066: CA root placeholder constants (`ACL-CA-KEY-LO` /
|
||||
`ACL-CA-KEY-HI`)
|
||||
- [x] `ACL-BOOT` stamps default ACL entries on all existing dictionary words
|
||||
- [x] `capsules/zuse.4th` loaded at end of `ACL.4th` capsule
|
||||
- [x] Zuse's words pinned by `ACL-ZUSE-BOOT` at load time
|
||||
|
||||
### Phase 4 — `init.4th` Opt-In Toggle (`master`) ✅ COMPLETE
|
||||
|
||||
- [x] `init.4th` has one commented-out line as the opt-in toggle:
|
||||
`\ S" ACL.4th" EXEC`
|
||||
- [x] Uncomment to enable full lockdown; leave commented for dev/open mode
|
||||
- [x] No other changes to `init.4th` required — `ACL.4th` is self-contained
|
||||
|
||||
### Phase 5 — POST Tests (`master`) ✅ COMPLETE
|
||||
|
||||
POST tests implemented in `src/test_runner/modules/acl_words_test.c`,
|
||||
registered in `src/test_runner/test_runner.c`. 800/800 passing.
|
||||
|
||||
- [x] POST test: `ACL-PIN` is one-way — mode cannot change after pin set
|
||||
- [x] POST test: inheritance — child entry has mode copied, pin cleared,
|
||||
ttl and decision reset
|
||||
- [x] POST test: emergency console bypass — `emergency_console=1` skips
|
||||
ACL check entirely
|
||||
- [x] POST test: STRICT mode — ACL re-evaluated on every execution
|
||||
- [x] POST test: TTL hot path — TTL > 0 bypasses re-evaluation
|
||||
- [x] POST test: adaptive accumulator — heat increase produces TTL increase
|
||||
- [x] POST test: privileged words pinned at boot remain pinned after
|
||||
`ACL-INIT-PRIMITIVES`
|
||||
|
||||
### Phase 6 — Isabelle/HOL Formal Verification (`master`) ✅ COMPLETE
|
||||
|
||||
Five `.thy` files in `proof/` alongside existing VM proofs:
|
||||
|
||||
- [x] `ACL_Pin_Monotone.thy` — pin bit is set-only; no operation clears it
|
||||
once set
|
||||
- [x] `ACL_Inherit_Clears_Pin.thy` — `ACL-INHERIT` always produces an entry
|
||||
with `acl_pinned = 0` regardless of source entry state
|
||||
- [x] `ACL_TTL_Bounded.thy` — TTL counter is bounded above by
|
||||
`ACL-TTL-COMPUTE` output; cannot grow unboundedly
|
||||
- [x] `ACL_Emergency_Bypass.thy` — when `emergency_console = 1` the
|
||||
allow/deny decision is never consulted
|
||||
- [x] `ACL_No_Escalation.thy` — a child VM cannot produce a pinned entry
|
||||
with higher privilege than its inherited mode
|
||||
|
||||
### Phase 7 — LithosAnanke Parity (COMPLETE — independently verified)
|
||||
|
||||
There is no separate `lithosananke` branch to merge/port to (post-split, this repo's `master`
|
||||
is the sole production line) — that framing is stale. Verified present directly in current
|
||||
`master`: `acl_recheck()`/`zuse_session`/`emergency_console` wiring confirmed in
|
||||
`src/starkernel/vm/vm_core.c`; the per-iteration `emergency_console = zuse_session ? 0 : 1`
|
||||
assignment confirmed in `src/starkernel/repl.c`; the old `!vm->zuse_session` ACL-check bypass
|
||||
confirmed absent from `src/vm.c`. See `.claude/CLAUDE.md`'s Word-Level ACL System section for
|
||||
the full verification writeup.
|
||||
|
||||
- [x] Verify `ACL.4th` loads cleanly in kernel context (freestanding)
|
||||
- [x] `ACL-BOOT` runs at kernel boot before first `BIRTH`
|
||||
- [x] `vm->emergency_console` wired to kernel REPL active flag
|
||||
- [x] `vm->zuse_session` wired to kernel Zuse console authentication path
|
||||
- [x] Three-arch acceptance: amd64, aarch64, riscv64 boot to `ok>` with ACL
|
||||
active and no regressions
|
||||
- [x] Acceptance logs — this repo's standing convention commits every acceptance boot's serial
|
||||
log under `logs/`, not a one-time Phase 7 action
|
||||
|
||||
### Phase 8 — PKI / Thumbdrive Authentication (FUTURE)
|
||||
|
||||
- [ ] Ed25519 challenge-response authentication for Zuse thumbdrive
|
||||
- [ ] `tools/mkcapsule` embeds real Ed25519 CA key into `ACL.4th` Block 2066
|
||||
at build time (replacing zero placeholder)
|
||||
- [ ] User minting: admin creates thumbdrive with CA-signed certificate + home
|
||||
block image
|
||||
- [ ] Lose the drive → admin mints a new one; no software recovery path by
|
||||
design
|
||||
- [ ] `zuse.4th` becomes the bootstrapper that validates the physical drive
|
||||
before granting Zuse session access
|
||||
@@ -1,24 +0,0 @@
|
||||
# docs/03-architecture/word-acl/
|
||||
|
||||
Design doc for the word-level ACL (access control) system.
|
||||
|
||||
- **[DESIGN.md](DESIGN.md)** — Full design: three ACL dispositions per word
|
||||
(`STRICT`, `TTL`, `PINNED`), the four `DictEntry` fields (`acl_ttl`,
|
||||
`acl_allow`, `acl_mode`, `acl_pinned`), the two VM flags
|
||||
(`emergency_console`, `zuse_session`), and the implementation split between
|
||||
C infrastructure and the pure-FORTH policy capsule `capsules/ACL.4th`.
|
||||
Status: implemented through Phase 6 on `master`; Phase 7 (LithosAnanke
|
||||
parity) is next.
|
||||
|
||||
Implementation files referenced by this design: `capsules/ACL.4th`,
|
||||
`capsules/zuse.4th`, `src/word_source/acl_words.c`,
|
||||
`src/test_runner/modules/acl_words_test.c`, and the ACL proof set in
|
||||
`proof/` (`ACL_Pin_Monotone.thy`, `ACL_Inherit_Clears_Pin.thy`,
|
||||
`ACL_TTL_Bounded.thy`, `ACL_Emergency_Bypass.thy`, `ACL_No_Escalation.thy`).
|
||||
|
||||
## See also
|
||||
|
||||
- [`proof/README.md`](../../../proof/README.md) — the ACL proof theory files.
|
||||
- [`capsules/README.md`](../../../capsules/README.md) — capsule files
|
||||
including `ACL.4th` and `zuse.4th`.
|
||||
- [Project root](../../../README.md)
|
||||
Reference in New Issue
Block a user