Status
Each component of Mini, graded by the strongest evidence for it.
This page is generated from the Honest state table of the repository README by website/gen-status.py, and a gate fails when it is stale. Edit the README, not this page.
Evidence classes: authored (source exists), compiled (Lean or Rust checked it), executed (it ran in a test or dev world), integrated (a native Host admitted it in a joined world), deployed (running on the public node for real users).
| Component | Evidence | Boundary |
|---|---|---|
| Native Host, shell, documents, journey J0–J8 | deployed | the public node runs the 2026-10-01 candidate (source 5688775a): the shell, documents (new, show, append, edit, link, backlinks) and boards; it has no rooms, chat, key rotation or proxy mode, and no outside member is enrolled (what it has and lacks: FRIENDS.md). Evidence: shell journey, J0–J8 89/89; node state read on 2026-10-03 (swarm Scout G, outside this repository). Main is not the candidate: the continuous journey runner at main 4795b657 (2026-10-04, runner table outside this repository) passes J0–J4, J6, J7 and JROTL and fails J5 and J8 (a stranger's attempt was not refused by the Host in 2 of 6 and 1 of 5 cases) and JROT (3 of 30 checks); the 10-01 pass is the candidate's, not main's, and the fix is open |
| Rooms, invitations, workroom template | integrated | on development worlds only, from lane builds: J15 and J17 pass in p-story and p-credit; not on the public node; room-scoped actions take seconds to minutes (Scout G: workroom template 224–270 s on a development world). ROOM-SCHEMA v2 landed in 6a173263; the private-rooms end-to-end driver (3aaa3cfd, journey row rooms) is red on main at 4795b657 (0 of 88 expected rows present) |
Chat (say, tail, topic, pin, react) | compiled | Rust code and tests in native/resource-client/src/chat.rs, and the JCHAT journey hook; no journey result in docs/evidence/ records JCHAT as PASS (the three 10-01 results mark it SKIPPED), so no recorded run has joined chat to a native Host (in-process operations: 336b7c0e) |
| Studio (edit, import, fork, history, preview) | authored; executed on lane builds only | client routes in native/resource-client/src/web/studio.rs and native/resource-client/src/workspace/studio.rs (2 focused tests); the loopback development servers that ran were built from lane branches, not from this commit; no member-reachable route; publication carries no authority; the prototype declarations still use the deleted Gen-1 shape and feed nothing (STUDIO-SOURCE-WORKSPACE.md); the preview is the Host's own Lean front end (31a9072e preview v2, a2454432 Lean front end) |
| Objective Bend Core4 semantics, machine, checker | compiled | soundness, preservation and completeness proved; the proofs are the ObjectiveProofs library, gated by scripts/check-objective-proofs.sh proofs (statement and axiom snapshot), not by the default build (details). Landed: completeness 1456f58e, forceWith and Plan-path soundness db7c0bc7, the statement and axiom snapshot gate 3204e85e |
| Objective Bend native admission | integrated on scratch worlds | native/resource-client/objective-native-acceptance.py all (journey row objective): publish, a signed invocation with an Accepted receipt, refusal rows r01-r13, reopen and replay; the receiver re-runs the Lean front end on the package and prices the declared envelope by the public tariff; not deployed (details). Landed: 31a9072e, 73223088 (tariff), 6df4602f (client and acceptance), 796d7d7a, a2454432 (Lean front end re-run by the receiver). Journey row objective PASS at main 4795b657 (17 rows, 2 readbacks) |
| Objective activities, object records, calls, sends, seats | integrated on scratch worlds (activities, object records, seats); calls and sends executed by lane drivers | every activity turn, invoke and deliverMessage included, is a signed native command (Host ops 210-214, mini activity), and seats have their own (215-219, mini seat); journey rows activity, objectrecord and seats run their drivers on scratch worlds; the call (C1-C8) and send (S1-S7) drivers exist and no journey row runs them (activities, seats). Landed: record, answer slots and resume contract 8194e09d; resume with view 67362781; paid exhaustion, disposal and abandonment d1ce7b0c; object record eac4b18c and de9c84f7; one public tariff bf28dd19; laws pin 2a7c372b; seats 6347dcb4 |
| SPK hosted apps | compiled (physical layer and Lean lifecycle); install, start, supervised restart and export integrated on development worlds | 44 of 44 rows of the 10-01 lane run (birth, install, share, start, a SIGKILLed generation replaced by the supervisor's STOP and continue-START, backup, stop, export). Failed-START recovery: spk-host grain supervise drives the Lean receiver (Kernel/ApplicationFailedStartRecoveryReceiver.lean) through Host ops 206–209 (native/spk-host/src/grain_export.rs; lookup and same-bytes resubmission unit-tested against a scripted Host), the code the live r2 world ran on 10-03 now on main; the deterministic journey rows (scripts/spk-platform/jspk1.sh failstart, an integration-qualification spk-host) are authored and have not run; no application has yet served a browser session (closest: EtherCalc co-editing over TLS with older binaries, 2026-10-02-spk-browser-tls) |
| Split tenancy (one account per friend, a key broker) | compiled; run on no box | mini-keys (1d4b683f) holds the seal key, provider keys and Discord secrets; mini key (73e06411), the Hermes controller (f991da1d) and the Discord entrance (7bb016a3) go through it; candidates ship it (b374fee3, 179f6bee). dregg-infra tenancy=split is built and on no box; the scratch run of its journey is not recorded (FRIENDS.md, 1784edf5) |
| Hermes in a room | executed | scripted provider on a private Store (J14, 2026-10-01); off on the public node |
| Discord entrance | executed | against a simulated Discord (2026-10-03-discord-world); under split tenancy it runs each line as the friend's account (7bb016a3); no Discord application exists and the entrance is inactive on the public node |
| Agreement mesh | compiled safety theorem; executed | safety over the Lean engine model; four replicas on one host, one failure domain; liveness not established (engine intake 02a4edd7, quiescent-leader and discovery fixes on main in 205ccbdb) |
| Traffic privacy | executed | one host, honest registrar, endpoint sees the plaintext call; no anonymity proof (roster enrollment d7b2f19b) |
| MPC / FHE | executed (research) | MPC: a width-8 adder over private inputs with per-dealer OS entropy, and a curious-holder transcript check over 8,067 frames, in native/private-backend tests (cf6a4c1d); FHE: none on main (the BFV consumer ran only upstream-Bend artifacts and was deleted on 2026-10-04) |
| Oblivious and zk execution of Objective Bend | authored, conditional | zk theorems take a refinement premise that is inhabited only for five literal programs, and native proof verification is not connected to the arithmetic relation (ZK.md, OBJECTIVE-BEND.md); the generic oblivious/arithmetic circuit stack has no Objective producer yet (a006d243: the tranche covers Core4) |
| Payments | executed (fixtures) | the pay journeys ran on private Stores with recorded Solana answers (deploy/pay/README.md); the enrolment address and rate (50 DREGG per week) are decided in enrol-terms.json but nothing is deployed: the pay watcher and roster sync are inactive on the public node, and no mainnet transaction has been made. Pay-to-enrol (mini join --solana, --wait, --renew) is documented in FRIENDS.md (b0bcb7d0, 243fb343) and the rate is one terms file (cb4235b6); journey steps JPAY1–JPAY4 run it on fixtures, and a known defect is open: the tariff counts hours, so the quoted week is 49.999992 DREGG, not 50 (cv 01a105c0-0292) |
Evidence rows cite runs of lane builds. Unless a row says otherwise, the run was not repeated at the commit this README describes. Dated, per-artifact evidence lives in docs/evidence/; update it there rather than copying counts into introductions.