Skip to content

Commit c632159

Browse files
hyperpolymathclaude
andcommitted
docs: update manifest + EXPLAINME for CLI consumer + package
- 0-AI-MANIFEST.a2ml: status → 2026-04-14, 4 ABI modules, Julia pkg, CLI consumer section, updated HOW TO RUN - EXPLAINME.adoc: mark both post-experiment items ✓, add new file entries (VCLProtocol.idr, Verisim.jl, vcl_server.jl, ffi/zig/), update run commands, add Phase 6 refactor note Co-Authored-By: Claude Sonnet 4.6 <noreply@anthropic.com>
1 parent 9b85352 commit c632159

File tree

2 files changed

+58
-16
lines changed

2 files changed

+58
-16
lines changed

verisim-modular-experiment/0-AI-MANIFEST.a2ml

Lines changed: 32 additions & 7 deletions
Original file line numberDiff line numberDiff line change
@@ -14,13 +14,15 @@ VCL consonance guarantees.
1414
the paved-road deployment. This experiment is a falsifier that produced
1515
a positive result: the octad IS divisible.
1616

17-
## CURRENT STATUS (2026-04-05)
17+
## CURRENT STATUS (2026-04-14)
1818

1919
- **Experiment status**: CLOSED with positive result. All 5 phases complete.
2020
- **Path B**: runtime-confirmed. Core = {Semantic, Temporal, Provenance}.
21-
- **Tests**: 145/145 green across 6 Julia test suites.
22-
- **Idris2 ABI**: 3 modules typecheck clean in Idris2 0.8.0.
23-
- **Overall completion**: 100% (research prototype).
21+
- **Tests**: 145/145 green across 6 Julia test suites (via `just test` / `Pkg.test()`).
22+
- **Idris2 ABI**: 4 modules typecheck clean (Types, VerisimCore, FederationContract, VCLProtocol).
23+
- **Julia package**: `Verisim` — `src/Verisim.jl`, `Project.toml v0.1.0`, `test/runtests.jl`.
24+
- **CLI consumer**: Zig binary (`ffi/zig/`) + Julia server (`src/vcl_server.jl`). 4/4 Zig unit tests green.
25+
- **Overall completion**: 100% (research prototype + consumer).
2426

2527
## KEY FINDING
2628

@@ -47,6 +49,22 @@ projection, Ed25519 attestation, coherence surface, LWW conflict resolution).
4749
- `Types.idr` — 8-shape enum + Core/Federable/Conditional classification
4850
- `VerisimCore.idr` — identity-core ABI (enrich, attest, verify)
4951
- `FederationContract.idr` — 5-clause contract + IsFederable predicate
52+
- `VCLProtocol.idr` — CLI stdio wire protocol (VCLQuery, VerdictResult, WellFormedExchange, A2ML framing constants)
53+
54+
### Julia Package: `src/Verisim.jl`
55+
56+
Package module. Loads impl files into `Main` via `Base.include`; exposes thin
57+
delegators: `prove`, `parse_vcl`, `Store`, `Manager`, `OctadId`, `SemanticBlob`,
58+
`enrich!`, `get_core`, all ProofClause constructors, Tropical types.
59+
60+
### CLI Consumer: `ffi/zig/` + `src/vcl_server.jl`
61+
62+
- `ffi/zig/src/verisim_cli.zig` — Zig 0.15 binary. Spawns Julia child process,
63+
pipes queries in, reads A2ML verdicts out. Subprocess = OS process isolation.
64+
No libjulia embedding. `VERISIM_PACKAGE_PATH` env override; default: 4 dirs up.
65+
- `src/vcl_server.jl` — Julia server script. Read by `julia --project=<pkg>`.
66+
Shared `Store`+`Manager` across session. Emits `[vcl-verdict]` A2ML blocks.
67+
- Build: `just cli-build-release` | Test: `just cli-test` | Query: `just cli-query "..."`
5068

5169
### Julia Reference Implementation: `impl/`
5270

@@ -81,11 +99,18 @@ projection, Ed25519 attestation, coherence surface, LWW conflict resolution).
8199
## HOW TO RUN
82100

83101
```bash
84-
# Idris2 ABI
102+
# Idris2 ABI (4 modules)
85103
idris2 --build verisim-modular-experiment.ipkg
86104

87-
# Julia test suites (6 files, 145 assertions)
88-
for f in test/*.jl; do julia --project=. $f; done
105+
# Julia package test suite (145 assertions, 6 suites)
106+
just test # or: julia --project=. -e 'using Pkg; Pkg.test()'
107+
108+
# Zig CLI unit tests
109+
just cli-test
110+
111+
# Build + run a VCL query end-to-end
112+
just cli-build-release
113+
just cli-query "PROOF INTEGRITY FOR abababababababababababababababababab"
89114
```
90115

91116
## LIFECYCLE HOOKS

verisim-modular-experiment/EXPLAINME.adoc

Lines changed: 26 additions & 9 deletions
Original file line numberDiff line numberDiff line change
@@ -48,16 +48,23 @@ the same data.
4848
== How do I run it?
4949

5050
```bash
51-
# Idris2 ABI — typechecks 3 modules
51+
# Idris2 ABI — typechecks 4 modules (includes VCLProtocol.idr)
5252
idris2 --build verisim-modular-experiment.ipkg
5353

54-
# Julia reference implementation — 70 assertions across 3 suites
55-
julia --project=. test/test_verisim_core.jl
56-
julia --project=. test/test_federation_parity.jl
57-
julia --project=. test/test_seams.jl
54+
# Julia package test suite — 145 assertions across 6 suites via Pkg.test()
55+
just test
56+
57+
# Zig CLI unit tests (verdict parser + protocol invariants)
58+
just cli-test
59+
60+
# Build the Zig CLI binary
61+
just cli-build-release
62+
63+
# Send a VCL query through the full CLI → Julia pipeline
64+
just cli-query "PROOF INTEGRITY FOR abababababababababababababababababab"
5865
```
5966

60-
Requirements: Julia 1.12+, Idris2 0.8.0, libsodium (auto-fetched via Sodium.jl).
67+
Requirements: Julia 1.10+, Idris2 0.8.0, Zig 0.15+, libsodium (auto-fetched via Sodium.jl).
6168

6269
== Where is everything?
6370

@@ -75,7 +82,16 @@ Requirements: Julia 1.12+, Idris2 0.8.0, libsodium (auto-fetched via Sodium.jl).
7582
|Central + subordinate proof obligations, and what's discharged.
7683

7784
|`src/Abi/`
78-
|Idris2 ABI definitions — `Types.idr`, `VerisimCore.idr`, `FederationContract.idr`.
85+
|Idris2 ABI definitions — `Types.idr`, `VerisimCore.idr`, `FederationContract.idr`, `VCLProtocol.idr` (CLI stdio wire protocol).
86+
87+
|`src/Verisim.jl`
88+
|Julia package entry point. Loads all impl modules into `Main` via `Base.include`, exposes thin delegators.
89+
90+
|`src/vcl_server.jl`
91+
|Julia stdio server for the CLI consumer. Spawned by the Zig binary; reads VCL from stdin, proves via `Verisim` package, emits A2ML verdicts.
92+
93+
|`ffi/zig/`
94+
|Zig CLI binary (`verisim`). Spawns `vcl_server.jl` as a subprocess; pipes queries through; forwards A2ML verdicts to stdout. `build.zig`, `build.zig.zon`, `src/verisim_cli.zig`.
7995

8096
|`impl/`
8197
|Julia reference implementation — `VerisimCore.jl`, `FederationManager.jl`,
@@ -133,9 +149,10 @@ All 5 phases + 3 deferred items complete. **Experiment closed, Path B confirmed.
133149

134150
Open post-experiment work (not blocking):
135151

136-
* Promote `impl/` to shippable `verisim-core` sibling package.
137-
* Zig FFI port of VerisimCore per hyperpolymath standard.
152+
* ✓ **Package**: `impl/` promoted to shippable `Verisim` Julia package (`src/Verisim.jl`, `Project.toml`, `test/runtests.jl`).
153+
* ✓ **CLI consumer**: `ffi/zig/` — Zig binary + `src/vcl_server.jl` Julia server + `src/Abi/VCLProtocol.idr` Idris2 ABI. Subprocess architecture (OS-level isolation per estate priority order). 4/4 unit tests green.
138154
* Formal Idris2-type-level non-interference proof at arbitrary N.
155+
* **Phase 6 refactor** (optional): migrate `impl/` from flat-include scaffold to proper Julia `src/` with `using ..Sibling` — removes `Main.X` cross-references and `Base.include(Main, f)`.
139156

140157
== What if the result had been negative?
141158

0 commit comments

Comments
 (0)