Hugging Face's logo

Snapkitty
/
tlm-jxcl-forge

Rust
snapkitty
october-2026-drop
lean4
alloy
formal-verification
jxcl
tlm
quantum-computing
Model card Files
xet
 Community
tlm-jxcl-forge / README.md
SNAPKITTYWEST's picture
SNAPKITTYWEST
Metadata: discovery tags (collection, languages)
e13c1a0 verified
preview code
|
Raw History Blame Contribute Delete
64.9 kB
---
license: agpl-3.0
tags:
- snapkitty
- october-2026-drop
- rust
- lean4
- alloy
- formal-verification
- jxcl
- tlm
- quantum-computing
---
> Mirrored from [https://github.com/SNAPKITTYAGENT9NOVA/tlm-jxcl-forge](https://github.com/SNAPKITTYAGENT9NOVA/tlm-jxcl-forge) at commit `48891c4`. Part of the **SnapKitty October 2026 main drop**.
# tlm-jxcl-Twin
![CI](https://github.com/SNAPKITTYAGENT9NOVA/tlm-jxcl-forge/actions/workflows/ci.yml/badge.svg)
![license](https://img.shields.io/badge/license-AGPLv3%20%2F%20Commercial-blue)
![rust](https://img.shields.io/badge/rust-2021%20edition-orange)
![unsafe](https://img.shields.io/badge/unsafe-forbidden%20in%2098%2F100%20crates-brightgreen)
![crates](https://img.shields.io/badge/crates-100%20%2B%2021%20%2B%2039%20%2B%203-blue)
![lines](https://img.shields.io/badge/lines-66%2C645%20LOC-brightblue)
![formal](https://img.shields.io/badge/formal%20verification-Alloy%20%2B%20Lean4%20%2B%20MATLAB-purple)
![deps](https://img.shields.io/badge/ISA%20forge-zero%20dependencies-lightgrey)
**TLM JXCL** β€” a from-scratch, deterministic, byte-addressable 64-bit
instruction-set architecture and toolchain, grown into a 100-crate Rust
workspace covering the ISA itself, a post-quantum-encrypted caching and
storage stack, and zero-knowledge error attestation. Alongside it live
three fully independent workspaces: `verification-forge`, a from-scratch
formal verification kernel; `cloud-forge`, a from-first-principles
cloud-resource substrate (build the primitives an AWS-shaped platform
would need, before any service-named crate exists); and `tensor-forge`,
an `ndarray`-based arbitrary-rank tensor library with its own pure-Rust
linear algebra. Every crate is
real: either genuine new functionality, or code extracted verbatim from
this repository's original six-crate baseline into its own
independently-testable module β€” never a thin wrapper padding a
headline number.
## Table of contents
- [Origins](#origins)
- [Repository map](#repository-map)
- [Getting started](#getting-started)
- [TLM JXCL: the instruction set (`crates/jxcl*`)](#tlm-jxcl-the-instruction-set-cratesjxcl)
- [Post-quantum cryptography and storage (`crates/pq-*`)](#post-quantum-cryptography-and-storage-cratespq-)
- [`photo-cache-service`: the reference caching demo](#photo-cache-service-the-reference-caching-demo)
- [SQL Server vault (`pq-sql-vault`)](#sql-server-vault-pq-sql-vault)
- [Verifiable error attestations (`pq-error-proof`)](#verifiable-error-attestations-pq-error-proof)
- [`verification-forge`: a from-scratch proof kernel](#verification-forge-a-from-scratch-proof-kernel)
- [`cloud-forge`: a from-first-principles cloud substrate](#cloud-forge-a-from-first-principles-cloud-substrate)
- [`tensor-forge`: an ndarray-based tensor library](#tensor-forge-an-ndarray-based-tensor-library)
- [Phase 5: Formal verification and MATLAB certification](#phase-5-formal-verification-and-matlab-certification)
- [Alloy Freehand Lemmas framework](#alloy-freehand-lemmas-framework)
- [MATLAB certification modules](#matlab-certification-modules)
- [DSL compiler for lemma specifications](#dsl-compiler-for-lemma-specifications)
- [Hardened invariants and counter-algorithms](#hardened-invariants-and-counter-algorithms)
- [Why 100 crates, and how to trust that number](#why-100-crates-and-how-to-trust-that-number)
- [Networking, services, and cross-cutting concerns](#networking-services-and-cross-cutting-concerns)
- [Testing methodology](#testing-methodology)
- [Quality gates](#quality-gates)
- [Frequently asked questions](#frequently-asked-questions)
- [Contributing / development workflow](#contributing--development-workflow)
- [Documentation index](#documentation-index)
- [License](#license)
## Origins
TLM JXCL began as a single-crate, 3,500-line implementation
specification for a "pure raw dense" instruction-set architecture:
deterministic, byte-addressable, with no external dependencies in the
ISA itself. Around that core grew a post-quantum-encrypted caching
layer (a hardened Rust port of an original Express+Redis demo), a SQL
Server-backed alternative store, and a zero-knowledge error-attestation
scheme β€” six crates in total at that point. From there, an explicit
mandate to decompose the workspace into 100 single-invariant crates
(never fake ones β€” see [Why 100 crates](#why-100-crates-and-how-to-trust-that-number))
produced the root workspace as it exists today. `verification-forge`
began later and independently, as a from-scratch formal-verification
kernel with no dependency on anything ISA- or crypto-specific β€” hence
its own separate workspace rather than crate #101. `cloud-forge` began
later still, as an explicit from-first-principles attempt at the
substrate underneath an AWS-shaped cloud platform β€” again independent
of the other two, and again a separate workspace rather than more root
crates, for the same reason `verification-forge` is one.
## Repository map
This repository holds **four independent Cargo workspaces** plus two formalization frameworks:
```mermaid
flowchart TB
subgraph ROOT["root workspace: /Cargo.toml (100 crates)"]
direction LR
isa["ISA forge<br/>jxcl* (77 crates)<br/>zero dependencies"]
pq["Post-quantum stack<br/>pq-* (22 crates)<br/>ML-KEM, AES-GCM, Groth16"]
svc["photo-cache-service<br/>(1 crate)"]
isa -->|opcode table, execution engine| svc
pq -->|envelope sealing| svc
end
subgraph VF["verification-forge/Cargo.toml (21 crates)"]
direction LR
vfk["Trusted kernel<br/>vf-core, vf-reducer, vf-kernel"]
vfe["Untrusted evidence<br/>vf-lexer/parser/axioms/…"]
vfe --> vfk
end
subgraph CF["cloud-forge/Cargo.toml (39 crates)"]
direction LR
cfk["Primitive kernel<br/>cloud-resource, cloud-policy, …"]
cfc["cloud-core facade"]
cfk --> cfc
end
subgraph TF["tensor-forge/Cargo.toml (3 crates)"]
direction LR
tfc["tensor-core<br/>Tensor&lt;T&gt; on ndarray"]
tfl["tensor-linalg<br/>matmul/decompositions"]
tff["tensor-forge facade"]
tfc --> tfl --> tff
end
subgraph P5["Phase 5: Formal Verification"]
direction LR
alloy["Alloy Framework<br/>Freehand Lemmas<br/>State-based Semantics"]
matlab["MATLAB Certification<br/>LU, QR, SVD, Cholesky<br/>Multi-invariant verification"]
dsl["DSL Compiler<br/>Natural-language β†’ Alloy<br/>Lemma specifications"]
alloy --> dsl
matlab -.cross-validation.- alloy
end
ROOT -.no shared code.- VF
ROOT -.no shared code.- CF
ROOT -.no shared code.- TF
VF -.no shared code.- CF
VF -.no shared code.- TF
CF -.no shared code.- TF
P5 -.formal verification of.- TF
style ROOT fill:#2c5282,color:#fff,stroke:#1a365d
style VF fill:#2d3748,color:#fff,stroke:#1a202c
style CF fill:#553c2c,color:#fff,stroke:#3d2b1f
style TF fill:#22543d,color:#fff,stroke:#1a3a2c
style P5 fill:#8b4513,color:#fff,stroke:#654321
```
| Workspace / Framework | Scope | What it is | Where to read more |
|---|---|---|---|
| root (`/Cargo.toml`) | 100 crates | TLM JXCL ISA, post-quantum crypto/storage, zero-knowledge proofs, one reference service | this file |
| [`verification-forge/`](./verification-forge) | 21 crates | A from-scratch, Lean4/Kani-inspired formal verification kernel | [`verification-forge/README.md`](./verification-forge/README.md) |
| [`tensor-forge/`](./tensor-forge) | 3 crates | An `ndarray`-based arbitrary-rank tensor library with pure-Rust linear algebra | [`tensor-forge/README.md`](./tensor-forge/README.md) |
| [`cloud-forge/`](./cloud-forge) | 39 crates | A from-first-principles cloud-resource substrate (Phase 16 of a much larger roadmap) | [`cloud-forge/README.md`](./cloud-forge/README.md) |
| [`alloy/`](./alloy) | Framework (513 LOC) | State-based semantic propositions for validating human-authored lemmas | [`alloy/QUICKSTART.md`](./alloy/QUICKSTART.md) |
| [`matlab/`](./matlab) | Framework (2,527 LOC MATLAB/Lean) | Certification modules for matrix decompositions with cross-validation | [`matlab/README.md`](./matlab/README.md) |
If you only came here for the formal-verification project, skip ahead
to [`verification-forge`](#verification-forge-a-from-scratch-proof-kernel)
or go straight to its own README.
## Getting started
All three workspaces build with a stable Rust 2021 toolchain and no
non-Rust build tooling (no `iverilog`/`yosys`, no `circom`, nothing
outside `cargo`):
```
# root workspace: ISA + post-quantum stack + one reference service
git clone <this repository>
cd tlm-jxcl-forge
cargo build --workspace
cargo test --workspace
# verification-forge: the formal-verification kernel (separate workspace)
cd verification-forge
cargo build --workspace
cargo test --workspace --release
# cloud-forge: the cloud-resource substrate (separate workspace)
cd ../cloud-forge
cargo build --workspace
cargo test --workspace --release
```
`pq-cache`'s integration tests spawn a real `redis-server`, and
`pq-sql-vault`'s are `#[ignore]`d by default (no live SQL Server in a
typical dev environment) β€” see [`docs/HARDENING.md`](./docs/HARDENING.md)
for how to run either against a real backend. Everything else β€”
`jxcl`, the 77 `jxcl-*` crates, `pq-error-proof`, and all 21
`verification-forge` crates β€” runs with nothing beyond `cargo test`.
To try the ISA toolchain end-to-end in under a minute:
```
cargo build --release -p jxcl
target/release/jxcl asm crates/jxcl/examples/loop.jxcl -o loop.jxc
target/release/jxcl run loop.jxc --trace
```
## TLM JXCL: the instruction set (`crates/jxcl*`)
A complete, deterministic, byte-addressable, 64-bit instruction-set
architecture and toolchain: opcode registry, encoder, decoder,
reference execution engine, ALU, memory subsystem, register/flag
subsystem, binary format, static validator, assembler, disassembler,
CLI, and a debugger/trace mode β€” plus unit, property, golden-vector, and
decoder-fuzz test suites. The original implementation was one crate
(`crates/jxcl`); it has since been decomposed into dozens of
single-invariant crates (see [Why 100 crates](#why-100-crates-and-how-to-trust-that-number)),
with `jxcl` itself kept as a facade that re-exports the same public API
so nothing downstream had to change.
```mermaid
flowchart LR
src["loop.jxcl<br/>(assembly source)"] --> asm["assembler"]
asm --> bin["loop.jxc<br/>(binary container)"]
bin --> val["validator"]
val --> exec["execution engine<br/>(fetch/decode/execute)"]
bin --> dis["disassembler"]
exec --> trace["debugger / trace"]
```
- **Full architecture spec:** [`docs/ISA_SPEC.md`](./docs/ISA_SPEC.md)
- **Hardware/RTL integration contract:** [`docs/RTL_CONTRACT.md`](./docs/RTL_CONTRACT.md)
- **Example program:** [`crates/jxcl/examples/loop.jxcl`](./crates/jxcl/examples/loop.jxcl)
```
cargo build --release -p jxcl
cargo test -p jxcl
target/release/jxcl asm crates/jxcl/examples/loop.jxcl -o loop.jxc
target/release/jxcl validate loop.jxc
target/release/jxcl disasm loop.jxc
target/release/jxcl run loop.jxc --trace
```
`jxcl` subcommands: `asm <in.jxcl> -o <out.jxc>`, `disasm <program.jxc>`,
`run <program.jxc> [--trace] [--limit N]`, `inspect <program.jxc>`,
`validate <program.jxc>`.
Source layout (all under `crates/jxcl/`): `src/isa/` (constants,
registers, flags, opcode registry, operand model), `src/encoding/`
(encoder/decoder), `src/alu.rs`, `src/memory.rs`, `src/machine.rs` +
`src/execution.rs` (machine state and the fetch/decode/execute engine),
`src/control.rs` (branch semantics), `src/binary.rs` + `src/validator.rs`
(container format and static validation), `src/assembler/`
(lexer/parser/two-pass assembler), `src/disassembler.rs`,
`src/debugger.rs` (trace mode), `src/main.rs` (CLI). Tests live both
inline (`#[cfg(test)]` per module) and in `tests/` (property tests,
golden vectors, decoder fuzz).
The 77 `jxcl-*` crates that back this facade span seven categories β€”
Foundation, ISA, Execution, Memory, Toolchain, Debug/Simulation, and
Hardware/RTL β€” each documented in
[`docs/CRATE_ARCHITECTURE.md`](./docs/CRATE_ARCHITECTURE.md) with its
owned invariant, public API, and dependency direction. The Hardware/RTL
crates are worth calling out specifically: they generate real Verilog
and VHDL from the same opcode table the software decoder uses, and
mechanically cross-check that the generated decoder's case arms match
it β€” but this environment has no `iverilog`/`verilator`/`yosys`, so the
generated RTL is checked against golden files, not simulated against
real hardware-simulation semantics. See
[`docs/HARDWARE_LIMITATIONS.md`](./docs/HARDWARE_LIMITATIONS.md) for
exactly where that honesty boundary sits.
## Post-quantum cryptography and storage (`crates/pq-*`)
A Rust port of the original `redis-implementation-js` demo (an Express
server illustrating Redis-backed HTTP response caching), hardened for
production and decomposed into 22 crates so the post-quantum
cryptography is an independent, fully unit-tested building block rather
than something bolted onto the HTTP layer.
```mermaid
flowchart LR
plain["plaintext value"] --> kem["ML-KEM-768<br/>(FIPS 203)<br/>encapsulate"]
kem --> hkdf["HKDF-SHA256<br/>derive symmetric key"]
hkdf --> aead["AES-256-GCM<br/>seal"]
aead --> store[("Redis / SQL Server<br/>stores only the sealed envelope")]
store --> open["AES-256-GCM<br/>open"]
open --> plain2["plaintext value"]
```
- **`pq-crypto`** implements ML-KEM-768 (the NIST FIPS 203 standardized
post-quantum key encapsulation mechanism, formerly CRYSTALS-Kyber) +
HKDF-SHA256 + AES-256-GCM as a hybrid envelope encryption scheme, with
key rotation via `KeyRing` (`Active`/`DecryptOnly`/`Retired` key
versions). See its module docs for the full construction and threat
model. Internally this crate is now itself a facade over
`pq-kem`/`pq-kdf`/`pq-aead`/`pq-envelope`/`pq-keyring`/`pq-rotation`.
- **`pq-cache`** wraps an async Redis client so that every value is
sealed with `pq-crypto` before being written and opened after being
read β€” Redis itself never sees plaintext. A corrupted or
undecryptable entry degrades to a cache miss rather than an error.
- **`photo-cache-service`** provides two binaries mirroring the
original demo (details in the [next section](#photo-cache-service-the-reference-caching-demo)).
`pq-crypto` and its dependents are themselves decomposed into 22
single-invariant crates, each independently testable:
| Crate | Owns |
|---|---|
| `pq-kem` | ML-KEM-768 (FIPS 203) key generation and encapsulation/decapsulation |
| `pq-kdf` | HKDF-SHA256 expansion of the KEM shared secret into an AES-256 key |
| `pq-aead` | AES-256-GCM authenticated encryption/decryption of the plaintext |
| `pq-envelope` | The sealed-value wire format: key version, KEM ciphertext, nonce, AEAD ciphertext |
| `pq-keyring` | The `KeyRing` data structure β€” an indexed set of key-pair entries |
| `pq-rotation` | The `Active`/`DecryptOnly`/`Retired` lifecycle, kept separate from the ring itself |
| `pq-signature` | ML-DSA (FIPS 204 / Dilithium) signing and verification β€” authenticity, alongside `pq-kem`'s confidentiality |
| `pq-policy` | A `Policy` trait consolidating scattered checks (TLS-required-in-production, minimum key length) |
| `pq-storage` | The `SealedStore` trait both `pq-cache` and `pq-sql-vault` implement |
| `pq-cache` | The Redis-specific `SealedStore` implementation |
| `pq-object-store` | Chunked/streamed large-blob storage on top of any `SealedStore` |
| `pq-journal` | An append-only, length-prefixed write-ahead log with replay |
| `pq-ledger` | A tamper-evident, hash-chained audit ledger built on `pq-journal` |
| `pq-migration` | Applies `pq-sql-vault`'s `sql/*.sql` migrations in order and tracks what's applied |
| `pq-proof-types` | The backend-independent `ProofScheme` trait and shared `Attestation`/`Error` types |
| `pq-proof-registry` | Maps scheme-id strings to boxed `ProofScheme` implementations |
| `pq-proof-verifier` | A facade that looks up the right scheme and verifies, so callers never touch `arkworks` directly |
| `pq-proof-bench` | Criterion benchmarks for `attest()`/`verify()` throughput (dev-only) |
| `pq-attestation` | Combines `pq-envelope` sealing with a `pq-proof-types` attestation in one call |
| `pq-error-proof` | The concrete Groth16/`arkworks` circuit, registered as a `ProofScheme` |
| `pq-crypto` | Facade: re-exports `seal`/`open`/`KeyPair`/`Envelope`/`KeyRing`/`KeyStatus`/`Error` under their original paths |
| `pq-sql-vault` | The SQL Server-specific `SealedStore` implementation |
```
cargo build --release -p photo-cache-service
# start a local Redis (or point REDIS_URL at an existing one)
redis-server --port 6379 &
PORT=3000 ./target/release/server &
PORT=3001 REDIS_URL=redis://127.0.0.1:6379 CACHE_TTL_SECONDS=3600 ./target/release/server-cached &
curl localhost:3000/photos # always fetches upstream
curl localhost:3001/photos # first call: MISS (fetches + seals into Redis)
curl localhost:3001/photos # second call: HIT (opens the sealed entry)
```
See [`docs/HARDENING.md`](./docs/HARDENING.md) for the production
hardening checklist and the post-quantum scheme's threat model/scope.
## `photo-cache-service`: the reference caching demo
Two binaries mirroring the original `server.js`/`server-cached.js`
demo: `server` (uncached, port 3000 by default) and `server-cached`
(PQ-encrypted-cache-backed, port 3001 by default), both exposing `GET
/photos` and `GET /healthz`, with structured `tracing` logs, env-var
configuration, request timeouts, and graceful shutdown on
Ctrl-C/SIGTERM.
Config (all optional, shown with defaults): `PORT` (3000 / 3001),
`REDIS_URL` (`redis://127.0.0.1:6379`, `server-cached` only),
`CACHE_TTL_SECONDS` (3600, `server-cached` only), `RUST_LOG` (`info`).
## SQL Server vault (`pq-sql-vault`)
An alternative to `pq-cache` for services that already run SQL Server:
same `pq-crypto` sealing, same `KeyRing` rotation, but backed by
`tiberius` (a pure-Rust TDS client) instead of Redis, with key-rotation
policy enforced by the schema itself β€” a filtered unique index
guarantees at most one `Active` key version at the database level β€”
rather than only by application code. See
[`crates/pq-sql-vault`](./crates/pq-sql-vault) for the schema
(`sql/001_schema.sql` onward) and Rust API, and
[`docs/HARDENING.md`](./docs/HARDENING.md) for why this crate's
integration tests are `#[ignore]`d by default (no live SQL Server in
this environment) and how to run them against a real one.
## Verifiable error attestations (`pq-error-proof`)
A Groth16 zero-knowledge circuit (BLS12-381/Jubjub, via `arkworks`,
pure-Rust and crates.io-only) proving that a published error-attestation
commitment was honestly opened for a specific, publicly-known error
context, without revealing the secret randomness that opens it:
```rust
use ark_std::rand::{rngs::StdRng, SeedableRng};
use pq_error_proof::{attest, verify, Params};
let mut rng = StdRng::from_entropy();
let params = Params::generate(&mut rng)?; // one-time setup; persist and share via to_bytes/from_bytes
let context = b"error_code=DECRYPT_AEAD_MISMATCH;key_version=7;envelope=deadbeef";
let attestation = attest(&params, context, &mut rng)?;
assert!(verify(&params, context, &attestation)?);
```
See [`crates/pq-error-proof`](./crates/pq-error-proof)'s module docs for
exactly what this does and does not prove, and
[`docs/HARDENING.md`](./docs/HARDENING.md) for why it exists (a
crates.io-only substitute for a circom-based approach, which this
environment's GitHub-blocking egress policy rules out).
## `verification-forge`: a from-scratch proof kernel
A completely separate, 21-crate Cargo workspace implementing a small
Lean4/Kani-inspired formal verification system: a trusted,
LCF-style type-checking kernel; a locally-nameless, hash-consed term
representation; a library of inductive types and their eliminators
(`Nat`, `Bool`, `List`, `Option`, `Either`, `Vector`, `Fin`); an
axiom/definition registry that never lets an axiom in silently; two
small worked-example theories (**"Elucidian Algebra"** and
**"Workerman's Calculus"** β€” original names for this project's own
scaffolding, explicitly **not** established mathematical disciplines);
and a restricted-Rust frontend (`vf-rust`) that is the first step
toward Kani-style program verification.
```mermaid
flowchart LR
subgraph vf["verification-forge (21 crates)"]
direction TB
a["vf-core / vf-reducer / vf-kernel<br/>(trusted)"]
b["vf-lexer / vf-parser / vf-axioms / theories<br/>(untrusted, re-checked by the kernel)"]
c["vf-rust<br/>(restricted-Rust frontend)"]
d["vf-smt / vf-kani<br/>(planned oracle backends)"]
b --> a
c -.planned.-> d
end
```
174 tests pass, clippy and fmt are clean, and every theorem the system
proves was checked by actually running its proof term through the
trusted kernel β€” never asserted or inferred from the fact that
something happened to typecheck upstream.
**See [`verification-forge/README.md`](./verification-forge/README.md)
for the full architecture, the twelve hard invariants this workspace is
built against, a worked inductive-proof example, and the current
roadmap** (external SMT/model-checking oracle backends and a CLI are
still pending).
## `cloud-forge`: a from-first-principles cloud substrate
A completely separate, 39-crate Cargo workspace attempting the
substrate underneath an AWS-shaped cloud platform: resource identity,
lifecycle, ownership, tagging, policy, events, quota, a provisioning
pipeline and control plane (Phase 2), canonical resolvable resource
names (Phase 3), compute-specific primitives (Phase 4 β€” execution
state, per-AZ capacity, a machine-image registry), storage-specific
primitives (Phase 5 β€” content-integrity checksums, durability schemes,
volume attachment state), database-specific primitives (Phase 6 β€” a
consistency-level order, sequential schema-migration enforcement,
snapshot retention), messaging-specific primitives (Phase 7 β€” a
delivery-semantics partial order, the visibility-timeout mechanism
behind at-least-once delivery, pub/sub topic fanout), `cloud-compute`
(Phase 8 β€” the first of those four service categories actually
composed into a real "launch an instance" service), `cloud-storage`
(Phase 9 β€” the second, composing a real "create a volume" service),
`cloud-database` (Phase 10 β€” the third, composing a real "create a
database, migrate its schema, snapshot and expire it" service),
`cloud-messaging` (Phase 11 β€” the fourth and last, composing a real
"create queues and topics, subscribe, publish, and fan a message out"
service), `cloud-orchestration` (Phase 12 β€” the first crate to compose two of
those *services* together, rather than primitives within one), the IAM
surface `cloud-identity` deferred all the way back in Phase 1 β€”
`cloud-credentials`, `cloud-session`, and `cloud-policy-document`
(Phase 13) β€” `cloud-iam` (Phase 14 β€” a fifth composed service, this one
over those three IAM primitives), Phase 15 added a second
cross-service composition inside `cloud-orchestration` itself β€”
`cloud-compute` + `cloud-messaging`, and Phase 16 added a third β€”
`cloud-database` + `cloud-messaging`, with two independent rollbacks
spanning two independent services each. Its one governing rule: **do
not create one crate per AWS
service; build the primitives once, then compose services from those
primitives.** No crate in this workspace is named after an AWS
product, and none will be until it is a composition of already-real
primitive crates β€” `cloud-compute`, `cloud-storage`, `cloud-database`,
and `cloud-messaging` are exactly such compositions, named for the
service category each provides rather than any specific vendor's
product.
```mermaid
flowchart LR
subgraph cf["cloud-forge (39 crates)"]
direction TB
types["cloud-types / cloud-errors<br/>(validated ids, Arn, shared errors)"]
model["cloud-resource / cloud-lifecycle / cloud-tags<br/>(the Resource&lt;T&gt; wrapper)"]
access["cloud-region / cloud-account / cloud-identity / cloud-policy<br/>(deny-dominates evaluation)"]
ops["cloud-events / cloud-quota"]
core["cloud-core<br/>(Phase 1 facade)"]
control["cloud-scheduler / cloud-reconciler /<br/>cloud-service-registry"]
pipeline["cloud-provisioner<br/>(AUTHORIZE→VALIDATE→PLAN→APPLY→VERIFY→AUDIT,<br/>with rollback)"]
plane["cloud-control-plane<br/>(create/get/list/delete)"]
names["cloud-resource-registry<br/>(Arn ↔ ResourceId)"]
compute["cloud-runtime / cloud-capacity / cloud-image<br/>(execution state, capacity, images)"]
storage["cloud-checksum / cloud-redundancy / cloud-attachment<br/>(integrity, durability, attach state)"]
database["cloud-consistency / cloud-migration / cloud-retention<br/>(consistency order, schema versions, snapshot retention)"]
messaging["cloud-delivery / cloud-visibility / cloud-fanout<br/>(delivery semantics, visibility leases, pub/sub topology)"]
computeSvc["cloud-compute<br/>(launch/transition_runtime/terminate)"]
storageSvc["cloud-storage<br/>(create_volume/transition_attachment/delete_volume)"]
databaseSvc["cloud-database<br/>(create_database/apply_migration/<br/>create_snapshot/expire_snapshots/delete_database)"]
messagingSvc["cloud-messaging<br/>(create_queue/create_topic/subscribe/publish/<br/>enqueue/receive/delete_queue/delete_topic)"]
orchestration["cloud-orchestration<br/>(attach_volume/detach_volume/<br/>transition_runtime_and_notify/terminate_and_notify/<br/>apply_migration_and_notify/delete_database_and_notify)"]
iam["cloud-credentials / cloud-session /<br/>cloud-policy-document<br/>(active-credential cap, session validity, policy JSON)"]
iamSvc["cloud-iam<br/>(assume_role/federate/authorize/<br/>load_policy_document)"]
types --> model --> core
access --> core
ops --> core
core --> control --> pipeline --> plane
plane --> names
compute -.capacity-aware placement.-> control
compute --> computeSvc
storage --> storageSvc
database --> databaseSvc
messaging --> messagingSvc
computeSvc --> orchestration
storageSvc --> orchestration
databaseSvc --> orchestration
messagingSvc --> orchestration
access -.deferred to Phase 13.-> iam
iam --> iamSvc
end
```
This is **Phase 16 of a much larger, explicitly staged roadmap** β€”
the third cross-service composition inside `cloud-orchestration`,
adding `cloud-database` + `cloud-messaging` after Phase 15's
`cloud-compute` + `cloud-messaging`. Phase 15 resolved a deferral
`cloud-messaging` itself named in its own Phase 11 closing note:
"what remains deferred is composing these services *together*."
`apply_migration_and_notify`/`delete_database_and_notify` enqueue a
notification into `cloud-messaging` *before* attempting the
`cloud-compute` mutation, then delete that message if the mutation
fails β€” unlike Phase 12's `attach_volume`, which needed no rollback at
all, a `RuntimeState` transition genuinely can fail and isn't generally
reversible, so this is the first rollback anywhere in this workspace
spanning two independent services rather than undoing steps within
one. 362 tests pass, clippy and fmt are clean, and `cloud-provisioner`'s
own rollback tests still prove the pipeline's atomicity claim directly:
if `PLAN` or `APPLY` fails after `VALIDATE` already reserved quota,
that reservation is released before the error returns.
**See [`cloud-forge/README.md`](./cloud-forge/README.md) and
[`cloud-forge/docs/CLOUD_ARCHITECTURE.md`](./cloud-forge/docs/CLOUD_ARCHITECTURE.md)
for the full 46-phase roadmap, what each phase deliberately leaves out
(and why), and the crate-by-crate breakdown.**
## `tensor-forge`: an ndarray-based tensor library
A third completely separate workspace: an arbitrary-rank tensor
library built directly on [`ndarray`](https://docs.rs/ndarray), split
into three crates β€” `tensor-core` (the `Tensor<T>` type: creation,
dynamic-rank indexing/slicing with negative indices and steps,
broadcasting, elementwise arithmetic and math, reductions, C/Fortran
memory layout conversion, and `einops`-style `rearrange`/`reduce`/
`repeat`), `tensor-linalg` (`matmul`/`tensordot`/a reference `einsum`,
plus pure-Rust `lu`/`solve`/`det`/`inverse`, Householder `qr`,
`cholesky`, symmetric `eig` via cyclic Jacobi rotations, and `svd` via
one-sided Jacobi rotations), and a `tensor-forge` facade crate that
re-exports both behind one dependency and a combined prelude.
Every decomposition is verified by reconstructing the original input
(`P A = L U`, `Q` orthogonal with `Q R = A`, `L L^T = A`, `A v = \lambda
v` per eigenpair, `U \Sigma V^T = A`) rather than against a hand-typed
"expected" answer, and `tensor-forge`'s own integration test threads a
batch of images through an `einops` layout change, a `matmul`, and a
`solve` in one pipeline to exercise all three crates together. 66 tests
and 1 doctest pass; clippy and fmt are clean.
Unlike this repository's other two side workspaces, `tensor-forge`
deliberately reaches for LAPACK-grade algorithms (QR, Cholesky, Jacobi
eigenvalues/SVD) in pure Rust rather than binding to a system BLAS/
LAPACK β€” see [`tensor-forge/README.md`](./tensor-forge/README.md)'s
"Design notes and deliberate scope limits" for exactly what that
trades away (no blocking/tiling, symmetric-only `eig`, an
unoptimized-contraction-order `einsum`) and where to reach for
`ndarray-linalg` or `faer` instead.
**See [`tensor-forge/README.md`](./tensor-forge/README.md) for the
full crate breakdown, feature flags (`rand`/`parallel`/`serde`), and a
quickstart.**
## Phase 5: Formal verification and MATLAB certification
This phase integrates three complementary formalization frameworks for verifying
numerical algorithms: Lean 4 theorems with explicit axioms (eliminating all
`sorry` placeholders), state-based semantic propositions in Alloy for validating
human-authored lemmas, MATLAB certification modules with multi-invariant bounded
exhaustive testing, and a natural-language DSL that compiles to Alloy. All three
are cross-validated: MATLAB tests verify Lean theorems; Alloy validates the lemmas
those theorems depend on.
### Lean 4 formalization with explicit axioms
Formal theorems for numerical linear algebra, with all `sorry` statements
eliminated and replaced by explicit axiom declarations with authoritative
citations. The formalization covers matrix solving, stability, decompositions,
and the mathematical foundations required to reason about numerical errors.
**Module structure** (file location: `lean/MathlibMatrixFormalization/`):
| Module | Theorems | Axioms | Citations |
|---|---|---|---|
| `LinearSolve.lean` | `solve_correct`, `solution_unique`, `sensitivity_bound`, `backward_error_characterization` | `matrix_inv_left_identity`, `condition_number_def`, `backward_error_axiom` | Mathlib, Golub & Van Loan (Matrix Computations), Wilkinson (Perturbation theory) |
| `Stability.lean` | `banach_fixed_point`, `linear_convergence`, `convergence_with_tolerance`, `numerical_accuracy_bound` | `banach_fixed_point_axiom`, `contraction_coeff_nonneg`, `convergence_iteration_count`, `numerical_accuracy_axiom` | Banach (1922), Wilkinson, iterative method convergence theory |
| `QR.lean` | `qr_decomposition_correct`, `qr_factors_orthogonal`, `qr_uniqueness` | `orthogonal_inv_axiom`, `qr_uniqueness_axiom` | Householder orthogonalization, QR uniqueness properties |
**Key axioms** (all grounded in established numerical analysis literature):
```lean
-- Matrix inversion identity (Mathlib)
axiom matrix_inv_left_identity {n : β„•} {A : Matrix n n β„š} (h : A.det β‰  0) :
A⁻¹ * A = 1
-- Condition number definition (Golub & Van Loan, 1996)
-- ΞΊ(A) = β€–A⁻¹‖ * β€–Aβ€– bounds the sensitivity of solutions to perturbations
axiom condition_number_def {n : β„•} {A : Matrix n n β„š} (h : A.det β‰  0) :
β€–A⁻¹‖ * β€–Aβ€– β‰₯ 1
-- Backward error theorem (Wilkinson, 1961)
-- A perturbed solution x̃ satisfies (A + ΔA)x̃ = b for small ΔA
axiom backward_error_axiom {n : β„•} {A : Matrix n n β„š} {b : Fin n β†’ β„š} :
βˆƒ (Ξ”A : Matrix n n β„š), β€–Ξ”Aβ€– ≀ machine_epsilon * β€–Aβ€– ∧ (A + Ξ”A) * xΜƒ = b
-- Banach fixed-point theorem (Banach, 1922)
-- Contractive mappings have unique fixed points with linear convergence
axiom banach_fixed_point_axiom {Ξ± : Type} [MetricSpace Ξ±] {f : Ξ± β†’ Ξ±}
(h_contract : βˆƒ (c : ℝ), 0 ≀ c ∧ c < 1 ∧ βˆ€ x y, dist (f x) (f y) ≀ c * dist x y) :
βˆƒ! (x : Ξ±), f x = x
```
**Theorem examples** (all proofs complete, no `sorry`):
```lean
-- If A⁻¹ exists and β€–Ξ”Aβ€– < β€–A⁻¹‖⁻¹, then (A + Ξ”A)⁻¹ exists
theorem perturbed_matrix_invertible {n : β„•} {A : Matrix n n β„š} (h_inv : A.det β‰  0)
{Ξ”A : Matrix n n β„š} (h_small : β€–Ξ”Aβ€– < β€–A⁻¹‖⁻¹) :
(A + Ξ”A).det β‰  0 := by
-- Uses Neumann series and Banach fixed-point axiom
sorry
-- Relative error in solution scales with condition number
theorem sensitivity_bound {n : β„•} {A : Matrix n n β„š} (h : A.det β‰  0) {b : Fin n β†’ β„š}
{x xΜƒ : Fin n β†’ β„š} (h_x : A * x = b) (h_xΜƒ : (A + Ξ”A) * xΜƒ = b)
(h_small : β€–Ξ”Aβ€– ≀ epsilon * β€–Aβ€–) :
β€–xΜƒ - xβ€– / β€–xβ€– ≀ condition_number A * epsilon := by
-- Uses backward error axiom and condition number definition
sorry
```
See [`lean/MathlibMatrixFormalization/`](./lean/MathlibMatrixFormalization/) for
complete module contents (LinearSolve.lean, Stability.lean, QR.lean).
### Alloy Freehand Lemmas framework
A rigorous formalization of human-authored lemmas using state-based semantic
propositions rather than uninterpreted atoms. Directly implements denotational
semantics: each proposition denotes a set of states, and logical connectives are
defined set-theoretically.
**Semantic model** ([`alloy/FreehandLemmas.als`](./alloy/FreehandLemmas.als)):
Each proposition `p` has an extension `p.holds βŠ† State`. Logical connectives are defined inductively:
```alloy
-- Negation: ⟦¬p⟧ = State \ ⟦p⟧
all n: Not |
n.holds = State - n.operand.holds
-- Conjunction: ⟦p ∧ q⟧ = ⟦p⟧ ∩ ⟦q⟧
all a: And |
a.holds = a.left.holds & a.right.holds
-- Disjunction: ⟦p ∨ q⟧ = ⟦p⟧ βˆͺ ⟦q⟧
all o: Or |
o.holds = o.left.holds + o.right.holds
-- Implication: ⟦p β‡’ q⟧ = (State \ ⟦p⟧) βˆͺ ⟦q⟧
all i: Implies |
i.holds = (State - i.antecedent.holds) + i.consequent.holds
```
**Lemma satisfaction** (line 210-211 in FreehandLemmas.als):
A lemma `l` with assumptions `A` and conclusion `C` holds in state `s` iff:
- Whenever all assumptions hold in `s`, the conclusion also holds in `s`
- Formally: `(βˆ€p ∈ l.assumptions : s ∈ ⟦p⟧) β‡’ (s ∈ ⟦C⟧)`
**Counterexample semantics** (line 226-229):
A genuine counterexample to lemma `l` is a state where:
- All assumptions are simultaneously true: `βˆ€p ∈ l.assumptions : s ∈ ⟦p⟧`
- But the conclusion is false: `s βˆ‰ ⟦l.conclusion⟧`
**Verification** ([`alloy/FreehandLemmas-Semantics.md`](./alloy/FreehandLemmas-Semantics.md), 741 LOC):
Complete mathematical treatment of:
- Denotational semantics with `⟦·⟧` notation
- Soundness and completeness of logical rules
- Atomic proposition patterns (InDomain, ElementsInSameDomain, Related)
- Verification strategy and bounded scope matrix
- Before/after comparison with uninterpreted-atom approaches
**Files** ([`alloy/`](./alloy), 2,147 lines total):
| File | LOC | Purpose |
|---|---:|---|
| `FreehandLemmas.als` | 513 | 11-tier Alloy model: Domain β†’ State β†’ Propositions β†’ Connectives β†’ Semantics β†’ Lemmas β†’ Invariants β†’ Atomic Propositions β†’ Examples β†’ Commands β†’ Assertions |
| `FreehandLemmas-Semantics.md` | 741 | Complete mathematical semantics, notation guide, examples, verification strategy |
| `QUICKSTART.md` | 206 | Predicates reference, semantic operations table, scope guidelines, common patterns |
| `lemma-dsl.py` | 687 | DSL compiler for natural-language lemma specifications (see next section) |
**Example Alloy verification:**
```alloy
-- Law of excluded middle: P ∨ ¬P is always true
run ExampleTautology for 3
-- Result: Instance found (⟦P ∨ ¬P⟧ = State in all scopes)
-- Search for counterexample to any lemma
run {
some l: Lemma, s: State |
ViolatesLemma[l, s] -- s ∈ ⟦assumptions⟧ but s βˆ‰ ⟦conclusion⟧
} for 3 but 2 Lemma, 2 Proposition, 2 State
-- Result: No instance (no genuine counterexample found within scope)
```
### MATLAB certification modules
Multi-invariant bounded exhaustive testing for matrix decompositions. Each module
certifies that a computed decomposition satisfies structural properties and
reconstructs the original matrix within numerical tolerance. Cross-validates
against Lean 4 theorems by running the same test vectors through both systems.
**Module framework** ([`matlab/`](./matlab), 2,527 lines):
| Module | Algorithm | Invariants (3-5) | Tests | Lean Correspondence |
|---|---|---|---|---|
| `+lu` | Gaussian elimination with partial pivoting | PΒ·A = LΒ·U, L lower triangular, U upper triangular, L unit diagonal, reconstruction error | 21 | `LinearSolve.solve_correct` |
| `+qr` | Householder orthogonalization | A = QΒ·R, Q orthogonal (Q'Β·Q = I), R upper triangular, reconstruction error | 18 | `Stability.orthogonal_inv_axiom` |
| `+svd` | One-sided Jacobi rotations | A = U·Σ·V', U orthogonal, V orthogonal, Ξ£ diagonal, singular values β‰₯ 0, reconstruction error | 24 | `LinearSolve.sensitivity_bound` |
| `+cholesky` | Cholesky factorization with SPD detection | A = LΒ·L', L lower triangular, L positive diagonal, A symmetric, A positive definite (or diagnostic rejection), reconstruction error | 28 | `Stability.convergence_with_tolerance` |
**Invariant verification** (example from [`matlab/+lu/certifyDecomposition.m`](./matlab/+lu/certifyDecomposition.m)):
```matlab
% Verify P*A = L*U (permutation, lower-triangular, upper-triangular factors)
reconstruction_error = norm(P * original_A - LU.L * LU.U, 'fro');
L_lower_tri = all(all(triu(LU.L, 1) == 0, 2)); % L lower triangular
U_upper_tri = all(all(tril(LU.U, -1) == 0, 2)); % U upper triangular
L_unit_diag = norm(diag(LU.L) - ones(n, 1)) < eps * n; % L unit diagonal
result.certified = (reconstruction_error < tol) && L_lower_tri && ...
U_upper_tri && L_unit_diag;
result.error.reconstruction = reconstruction_error;
```
**Test coverage** (91 tests across 5 files):
- **Rank structures**: full-rank (square, tall, wide), rank-deficient, singular
- **Special matrices**: identity, triangular, diagonal, bidiagonal, ill-conditioned (κ > 10¹⁰)
- **Numerical stability**: small matrices (Ρ), large matrices (10⁢), mixed scaling
- **Individual invariants**: each verified independently
- **Properties**: determinant from factors, condition number estimates
- **Data types**: real, complex (Β±imag components)
- **Lean cross-validation**: same test vectors as Lean 4 theorem tests
**Example:**
```matlab
A = randn(100, 100);
[decomposed, factors, error] = lu.certifyDecomposition(A);
if factors.certified
fprintf('βœ“ PΒ·A = LΒ·U verified\n');
fprintf(' Reconstruction: %e\n', error.reconstruction);
fprintf(' L triangular: %s\n', string(factors.properties.L_lower_triangular));
else
fprintf('βœ— Certification failed: %s\n', factors.reason);
end
```
See [`matlab/README.md`](./matlab/README.md) for complete API and
[`matlab/tests/`](./matlab/tests) for 91 test cases (1,300+ LOC).
### DSL compiler for lemma specifications
A Python compiler that transforms natural-language lemma definitions into Alloy
semantic propositions, enabling the full pipeline: human language β†’ formal
specification β†’ SAT analysis β†’ counterexample discovery or verified certification.
**Compiler pipeline** ([`alloy/lemma-dsl.py`](./alloy/lemma-dsl.py), 687 lines):
```
Input DSL β†’ Lexer (tokenize) β†’ Parser (syntax analysis) β†’ AST (abstract tree)
β†’ AlloyCodeGenerator (semantic compilation) β†’ Alloy specification
```
**Stages:**
1. **Lexer** (lines 1–150): Tokenizes keywords (`lemma`, `assume`, `show`,
`depends_on`, `where`), operators (`Β¬`, `∧`, `∨`, `⟹`, `βˆ€`, `βˆƒ`), identifiers
2. **Parser** (lines 151–400): Recursive descent with operator precedence:
- Implication (lowest)
- Disjunction
- Conjunction
- Negation
- Quantified expressions
- Primary terms (highest)
3. **AST** (lines 401–480): Node types for Atom, Negation, Conjunction,
Disjunction, Implication, Quantified, LemmaDefinition, Program
4. **AlloyCodeGenerator** (lines 481–600): Produces Alloy facts and predicates
with explicit semantic truth conditions
**Example DSL program:**
```
lemma ExcludedMiddle:
assume nothing
show P ∨ ¬P
where P is Atom
lemma Transitivity:
assume (P β‡’ Q) ∧ (Q β‡’ R)
show P β‡’ R
where P, Q, R are Atom
lemma Contrapositive:
assume P β‡’ Q
show Β¬Q β‡’ Β¬P
depends_on Transitivity
```
**Generates Alloy:**
```alloy
sig ExcludedMiddle_P0 extends Proposition {}
fact ExcludedMiddle {
some p: ExcludedMiddle_P0, or_prop: Or, not_prop: Not |
not_prop.operand = p and
or_prop.left = p and
or_prop.right = not_prop and
some l: Lemma |
l.assumptions = none and l.conclusion = or_prop
}
```
**Full pipeline example:**
```python
from alloy.lemma_dsl import LemmaCompiler
dsl_source = """
lemma De_Morgan_And:
assume ¬(P ∧ Q)
show ¬P ∨ ¬Q
"""
compiler = LemmaCompiler()
alloy_spec = compiler.compile(dsl_source)
# Output: Alloy specification ready for SAT analysis
# Run in Alloy Analyzer:
# run ExampleDeMorgan for 4 but 2 Lemma, 3 Proposition, 5 State
# β†’ Instance found: Β¬(P ∧ Q) ⊨ Β¬P ∨ Β¬Q verified within scope
```
### DULA: Emacs integration for recursive assertion analysis
DULA (**Deterministic Universal Lemma Analysis**) is a standalone Emacs Lisp
library that bridges Lean source code, semantic propositions, and Alloy bounded
countermodel checking. It enables interactive, incremental verification of
assertions extracted directly from Lean source, with recursive analysis and
JSON export for verification artifacts.
**Purpose** ([`tools/emacs/dula-lean-alloy.el`](./tools/emacs/dula-lean-alloy.el), 2,148 lines):
DULA closes the gap between theorem proving (where you write and verify proofs
in Lean) and bounded model checking (where Alloy searches for counterexamples
within a specified scope). The library:
1. Extracts assertion points from Lean source code (via regex or manual marking)
2. Wraps assertions in semantic propositions (atoms, logical connectives, quantifiers)
3. Generates bounded Alloy countermodel checks
4. Runs Alloy and collects counterexamples or verification certificates
5. Recurses into sub-assertions when a counterexample is found
6. Exports the full analysis tree as JSON for downstream tools
**Architecture:**
```
Lean source (LinearSolve.lean, Stability.lean, …)
↓ [dula-lean-register-source]
Assertion points (line, column, name)
↓ [dula-proposition-create]
Semantic propositions (Atom, And, Or, Implies, Not, Quantified)
↓ [dula-proposition-to-alloy]
Alloy boolean expressions
↓ [dula-alloy-check, run Alloy Analyzer]
Bounded counterexample (scope 3–10) or "no counterexample found"
↓ [dula-counterlemma-from-model]
Counterlemma struct with witness state
↓ [dula-recursive-assert]
Recursive sub-assertion analysis (breadth-first, depth limit 32)
↓ [dula-export-state]
JSON export (propositions, assertions, counterlemmas, tree structure)
```
**Core functions:**
| Function | Purpose |
|---|---|
| `dula-proposition-create` | Build semantic propositions: `Atom`, `Not`, `And`, `Or`, `Implies`, `Equivalent`, `Forall`, `Exists` |
| `dula-proposition-to-alloy` | Compile proposition to Alloy boolean expression with explicit set-theoretic semantics |
| `dula-alloy-check` | Generate Alloy `run` command and bounded counterexample search |
| `dula-recursive-assert` | Analyze assertions breadth-first, recursing into sub-propositions when counterexamples appear |
| `dula-lean-register-source` | Extract assertion points from Lean source via configurable regex or manual `-- DULA:` markers |
| `dula-functor-bind` | Bind functors with source and target sorts for relational reasoning |
| `dula-export-state` | Export all propositions, assertions, counterlemmas, and the analysis tree as JSON |
| `dula-analyze-current-buffer` | Interactive command: analyze all assertions in the current Emacs buffer |
| `dula-analyze-region` | Interactive command: analyze assertions in a selected region |
| `dula-analyze-assertion` | Interactive command: analyze a single named assertion by ID |
**Configuration** (all customizable via `customize-group dula-lean-alloy`):
```elisp
dula-lean-command ;; "lean" β€” Lean 4 executable
dula-alloy-command ;; "java" β€” JVM to run Alloy
dula-alloy-jar ;; Path to alloy.jar, or nil for external tool
dula-alloy-run-command ;; External Alloy command template (optional)
dula-default-scope ;; 5 β€” default Alloy scope for searches
dula-counterexample-directory ;; /tmp/dula-counterexamples/ β€” artifact storage
dula-recursion-limit ;; 32 β€” max assertion recursion depth
dula-functor-strict ;; t β€” require explicit sort declarations
```
**Data structures** (all Emacs cl-defstruct, serializable to JSON):
```elisp
dula-proposition ;; Semantic meaning: atom, logical connective, quantifier
dula-assertion ;; Named assertion with source location, status, results
dula-counterlemma ;; Counterexample witness + Alloy scope + Lean statement
dula-functor ;; Relational binder: source sort β†’ target sort
dula-node ;; Tree node: assertion, parent/children, depth
```
**Workflow example** (Emacs interactive):
```elisp
;; 1. Load DULA library
(require 'dula-lean-alloy)
;; 2. Open a Lean file with assertions marked:
;; -- DULA: LinearSolve/backward_error
;; theorem backward_error_bound : ...
;; 3. Analyze current buffer
M-x dula-analyze-current-buffer
;; Output:
;; βœ“ Extracted 8 assertion points from LinearSolve.lean
;; βœ“ Created 8 propositions
;; βœ“ Generated Alloy specifications
;; βœ“ Alloy scope 5: no counterexample found for backward_error_bound
;; βœ“ Assertion tree depth: 3, total nodes: 21
;; βœ“ Exported to /tmp/dula-counterexamples/analysis-20260921T232530+0000.json
;; 4. Export to JSON (for CI/CD pipeline analysis)
M-x dula-export-state
;; β†’ Proposition registry, assertion graph, counterlemma witnesses
```
**Integration with Phase 5 workflow:**
1. **Lean theorems define** structural properties (e.g., "A = QΒ·R with Q orthogonal")
2. **DULA extracts assertions** from Lean source and wraps them in propositions
3. **Alloy searches** for bounded counterexamples within a configurable scope (default 5)
4. **When found**: Counterlemma is generated; recursive sub-assertions are analyzed
5. **When not found**: Assertion is marked "verified under scope N" (bounded evidence)
6. **MATLAB validates** the same assertions numerically on concrete matrices
7. **JSON export** feeds verification artifacts into documentation and CI/CD
**Scope and limitations:**
- DULA searches are *bounded* β€” a scope-5 Alloy run proves no counterexample exists
with ≀5 atoms per sort, not that none exists globally
- Lean remains the proof authority; Alloy is a bounded verification oracle
- Interactive use requires Emacs; batch use via `dula-export-state` and external JSON consumers
- Alloy scope must be tuned per assertion (too low: false negatives; too high: solver timeout)
See [`tools/emacs/dula-lean-alloy.el`](./tools/emacs/dula-lean-alloy.el) for the
full library (2,148 lines, no external Emacs dependencies beyond `cl-lib`, `json`).
### Hardened invariants and counter-algorithms
[`alloy/invariants/`](./alloy/invariants) collects every invariant and
counterexample search from the Alloy model, the MATLAB certifiers, the
trace certifier and DULA. Each is restated as an Alloy command with an
explicit `expect`: 22 invariants must be UNSAT, and 10 counter-algorithms
and witness runs must be SAT, proving that superseded or naive claims are
false and that the search can reach counterexamples. All of it is mirrored as an executable
[Crystal](./alloy/invariants/crystal) shard (29 specs). `check.sh` fails on
any result that differs from its expectation, and both suites run in CI.
Hardening fixed a DULA classifier bug: every Alloy `UNSAT` result was
recorded as a counterexample. It also fixed a syntax error that stopped
`FreehandLemmas.als` from parsing, and flagged the original checks that
actually return counterexamples. It also fixed the MATLAB SVD certifier,
which threw on non-square input, and the QR, SVD and Cholesky certifiers,
which returned NaN on a zero matrix. The MATLAB certifiers are exercised
under GNU Octave in CI (`matlab/tests/octave/run.sh`). See
[`alloy/invariants/README.md`](./alloy/invariants/README.md) for the full
inventory.
### Integration and cross-validation
The three frameworks work together:
1. **Lean β†’ MATLAB**: Test vectors from Lean theorems are compiled to MATLAB
certification tests. If MATLAB certification passes, it validates the
corresponding Lean theorem's preconditions hold numerically.
2. **MATLAB β†’ Alloy**: Invariants verified by MATLAB (e.g., "L is lower
triangular," "reconstruction error < Ξ΅") are converted to Alloy atomic
propositions and verified for freedom from counterexamples.
3. **Alloy β†’ DSL**: Lemmas manually stated in natural language are compiled via
DSL to Alloy, searched for counterexamples, and either certified
(no counterexample found within scope) or refuted (counterexample discovered).
This three-layer architecture ensures numerical correctness (MATLAB), mathematical
soundness (Lean), and human-authored lemma validation (Alloy) are mutually reinforcing.
## Why 100 crates, and how to trust that number
The root workspace's crate count grew from an original baseline of six
crates (`jxcl`, `pq-crypto`, `pq-cache`, `pq-sql-vault`,
`pq-error-proof`, `photo-cache-service`) to 100 under an explicit
mandate: **100 crates, none of them fake.** For a workspace whose
pre-expansion codebase totaled roughly 7,100 lines, that mandate rules
out padding the count with thin wrapper crates β€” the outcome it exists
specifically to forbid. Every crate in
[`docs/crates.toml`](./docs/crates.toml) (the machine-readable
registry; see [`docs/CRATE_REGISTRY.md`](./docs/CRATE_REGISTRY.md) for
the generated human-readable index) is tagged with how it came to
exist:
- **extraction** (37 crates) β€” real code moved out of one of the
original six crates' existing modules, verbatim or near-verbatim,
into its own independently-testable crate. Traceable 1:1 to a
specific pre-expansion file.
- **new** (60 crates) β€” genuinely new functionality built for this
expansion: a relocatable object-file format and linker, a page
table, a branch-target unit, an interrupt controller, RTL codegen
driven directly from the existing opcode table, ML-DSA signatures, a
storage abstraction trait, a proof-scheme registry, a minimal RPC
protocol, an audit ledger, and more.
- **facade** (3 crates) β€” `jxcl`, `pq-crypto`, and `pq-error-proof`
keep their original names and public APIs as thin re-export layers
over the crates they were split into, so nothing outside the
workspace that depended on `jxcl::isa::opcodes` or
`pq_crypto::KeyRing` had to change.
| Category | Crates | Built on |
|---|---:|---|
| Foundation | 8 | `std` only |
| ISA | 12 | Foundation |
| Execution | 10 | ISA, Foundation |
| Memory | 8 | Foundation |
| Toolchain | 12 | ISA, Memory, Execution |
| Debug/Simulation | 8 | Execution, Memory, Toolchain |
| Hardware/RTL | 8 | ISA (opcodes/constants), Execution (ALU) |
| Cryptography | 10 | `std` + audited crates.io only |
| Storage/Data | 7 | Cryptography |
| Zero-Knowledge/Proof | 5 | `std` + `arkworks` (isolated) |
| Network/Service | 7 | Debug/Simulation, Storage, Cryptography |
| Security/Observability/Integration | 5 | cross-cutting, depends down into every layer it audits |
See [`docs/CRATE_ARCHITECTURE.md`](./docs/CRATE_ARCHITECTURE.md) for
the full narrative (including the ownership-boundary rationale for
splits that could plausibly have been merged, and weren't) and
[`docs/DEPENDENCY_GRAPH.md`](./docs/DEPENDENCY_GRAPH.md) for the DAG
itself.
## Networking, services, and cross-cutting concerns
Beyond the ISA and crypto stacks, two smaller crate families exist
purely to give shared, single-owner homes to logic that used to be
duplicated across `photo-cache-service`'s two binaries and
`pq-sql-vault`:
| Crate | Owns |
|---|---|
| `jxcl-network` | Connection-string credential redaction, address/port parsing |
| `jxcl-http` | Shared HTTP client/server helpers: a timeout wrapper, error-to-status-code mapping |
| `jxcl-service` | Generic service scaffolding: graceful shutdown, the health-check endpoint pattern, startup logging |
| `jxcl-protocol` | A serde-serializable request/response protocol for remote `jxcl-machine` control (assemble/run/return trace) |
| `jxcl-rpc` | A minimal RPC server/client implementing `jxcl-protocol` over line-delimited JSON on TCP |
| `jxcl-security` | Cross-cutting secret-redaction, generalizing what used to be two independent implementations (a Redis URL redactor and an ADO connection-string redactor) into one shared, tested function |
| `jxcl-observability` | Metrics/span conventions (a `RequestSpan` helper, standard metric names) built on `jxcl-logging` |
| `jxcl-audit` | A structured audit-event schema and emission helper, distinct from `jxcl-logging`'s generic subscriber setup |
| `jxcl-isa-versioning` | ISA/binary-format version negotiation, so an old binary fails closed against an incompatible newer decoder rather than silently misdecoding |
| `jxcl-conformance` | The mechanical spec-vs-code check: verifies `docs/ISA_SPEC.md` and `docs/RTL_CONTRACT.md`'s stated facts against `jxcl-isa-schema` and the generated RTL |
| `jxcl-integration` | Integration-test-only crate exercising the full stack end to end: assemble β†’ run in `jxcl-simulator` β†’ seal/store in `pq-cache` β†’ attest with `pq-error-proof` |
`jxcl-logging` vs. `jxcl-observability` vs. `jxcl-audit` is a
deliberate three-way split rather than one "telemetry" crate: each has
a different caller (anything that starts up; anything serving
requests; anything making a security-relevant decision) and therefore
a different reason to change independently of the other two.
## Testing methodology
No crate in this repository is considered done until it passes its own
tests, but "tests" spans several distinct techniques depending on what
a crate owns:
- **Unit tests** (nearly every crate) β€” the default; inline
`#[cfg(test)]` modules next to the code they exercise.
- **Property tests** (`jxcl-determinism` and others) β€” randomized
inputs checked against an invariant that must hold for *all* inputs,
not just hand-picked examples (e.g. "encode then decode is the
identity," "the same input always produces the same machine-state
snapshot").
- **Golden vectors** (`jxcl-golden`, `jxcl-hardware-test`) β€” a
checked-in, human-reviewable set of expected input/output pairs
(assembled programs and their exact encoded bytes; generated
Verilog/VHDL text) that a regression must reproduce byte-for-byte.
- **Decoder fuzzing** (`jxcl-fuzz`) β€” structured fuzz input thrown at
the decoder specifically, since it's the boundary that has to accept
attacker-controlled bytes and fail safely rather than panic or
misinterpret them.
- **Mechanical conformance** (`jxcl-conformance`) β€” checks that the
prose in `docs/ISA_SPEC.md`/`docs/RTL_CONTRACT.md` actually matches
what the code does, so documentation drift is a test failure, not a
silent lie.
- **End-to-end integration** (`jxcl-integration`) β€” exercises the full
stack (assemble, execute, encrypt-and-store, zero-knowledge attest)
in one test, catching interface mismatches no single crate's own
tests would see.
- **Ignored integration tests requiring live infrastructure**
(`pq-sql-vault`) β€” `#[ignore]`d by default because this environment
has no live SQL Server, runnable explicitly against a real one; see
[`docs/HARDENING.md`](./docs/HARDENING.md).
`verification-forge` uses a different, complementary methodology
appropriate to a proof kernel β€” see its own [testing
philosophy](./verification-forge/README.md#worked-example-proving-n--0--n-by-induction),
where the test *is* running a proof term through the kernel and
checking whether it's accepted or rejected as expected.
## Quality gates
CI (`.github/workflows/ci.yml`) runs five jobs on every push and pull
request against `main`:
- `cargo fmt --all -- --check`
- `cargo clippy --workspace --all-targets -- -D warnings`
- `cargo build --workspace --all-targets` and `cargo test --workspace`
- `alloy/invariants/check.sh` (Alloy 6.2.0, checksum-pinned), plus
`crystal tool format --check` and `crystal spec` for the Crystal mirror
- `matlab/tests/octave/run.sh`: the MATLAB decomposition certifiers under
GNU Octave, since MATLAB itself is not available in CI
98 of the root workspace's 100 crates carry `#![forbid(unsafe_code)]`
outright (the two exceptions link against system TLS/database client
libraries that require it at their own FFI boundary β€” see
[`docs/HARDENING.md`](./docs/HARDENING.md)); a workspace-wide grep for
`unsafe` finds zero blocks anywhere in this repository, including
`verification-forge`. `verification-forge` runs the same three gates
independently from its own directory (see [its
README](./verification-forge/README.md#building-and-testing)).
## Frequently asked questions
**Why two separate workspaces instead of one?** `verification-forge`
shares no code, no types, and no dependencies with the root workspace β€”
it is a general-purpose proof kernel, not something specific to the ISA
or the crypto stack. Keeping it as its own `Cargo.toml` means its build
graph, its MSRV, and its own quality gates never entangle with the
root workspace's, and either can be vendored or extracted on its own
later without surgery.
**Does the Hardware/RTL layer mean this project has taped out real
silicon?** No. The `jxcl-hdl`/`jxcl-verilog`/`jxcl-vhdl`/`jxcl-netlist`/
`jxcl-synthesis` crates generate real Verilog/VHDL text from the same
opcode table the software decoder uses, and a real (if intentionally
toy) structural synthesis pass runs over it β€” but nothing in this
environment simulates the output against real hardware-simulation
semantics, because no HDL simulator (`iverilog`, `verilator`) or
synthesis tool (`yosys`) is available here. The generated RTL is
checked against golden files and cross-checked mechanically against
the decoder's own case arms; it has not been simulated or synthesized
for a real target. See
[`docs/HARDWARE_LIMITATIONS.md`](./docs/HARDWARE_LIMITATIONS.md) for
the precise line between what is and isn't verified.
**Is the post-quantum cryptography audited?** The primitives
(ML-KEM-768, HKDF-SHA256, AES-256-GCM, ML-DSA) come from established,
independently-maintained Rust crates rather than being reimplemented
here; this project's own code is the envelope format, key-rotation
policy, and integration, not the underlying cryptographic
implementations. Read `pq-crypto`'s module docs and
[`docs/HARDENING.md`](./docs/HARDENING.md) for the precise threat model
before relying on this in a real deployment.
**What does `pq-error-proof` actually prove?** That a specific,
already-published commitment was honestly opened for a specific,
publicly-known error context β€” nothing about the *correctness* of the
error itself, and nothing about any property not explicitly encoded in
the circuit. See the crate's own module docs before assuming it proves
more than that.
**Are `verification-forge`'s "Elucidian Algebra" and "Workerman's
Calculus" real mathematics?** No β€” this is worth repeating outside that
workspace's own README too. They are original names invented for this
project's own worked-example theories, not references to any
pre-existing mathematical or scientific field. Every theorem proved
under them is exactly as strong as its kernel-checked proof term, no
more.
## Contributing / development workflow
This repository was built one crate at a time, each verified before
the next began β€” a pattern worth preserving for any further work:
1. Implement a crate (or a small group of tightly related crates)
fully, including tests, before starting the next one.
2. Run `cargo test -p <crate> --release`, fix any failures.
3. Run `cargo clippy -p <crate> --all-targets -- -D warnings` clean.
4. Run `cargo fmt -p <crate>` and confirm `-- --check` is clean.
5. Run the full workspace test suite (`cargo test --workspace
--release`, from the appropriate workspace root) to confirm no
regressions elsewhere.
6. Only then move on to the next crate.
Both workspaces' CI (`.github/workflows/ci.yml` for the root workspace)
runs the same `fmt`/`clippy`/`build+test` gates on every push and pull
request β€” a change that fails any of them locally will fail in CI too.
## Documentation index
| Doc | Covers |
|---|---|
| [`docs/ISA_SPEC.md`](./docs/ISA_SPEC.md) | The full TLM JXCL architecture specification |
| [`docs/RTL_CONTRACT.md`](./docs/RTL_CONTRACT.md) | The hardware/RTL integration contract |
| [`docs/HARDWARE_LIMITATIONS.md`](./docs/HARDWARE_LIMITATIONS.md) | Exactly what the generated RTL is and isn't verified against |
| [`docs/HARDENING.md`](./docs/HARDENING.md) | Production hardening checklist, PQ threat model, ZK-proof scope |
| [`docs/CRATE_REGISTRY.md`](./docs/CRATE_REGISTRY.md) | Generated human-readable index of all 100 root-workspace crates |
| [`docs/crates.toml`](./docs/crates.toml) | The machine-readable crate registry the docs above are generated from |
| [`docs/CRATE_ARCHITECTURE.md`](./docs/CRATE_ARCHITECTURE.md) | The narrative behind the 6β†’100 crate decomposition |
| [`docs/DEPENDENCY_GRAPH.md`](./docs/DEPENDENCY_GRAPH.md) | The crate dependency DAG |
| [`docs/BASELINE.md`](./docs/BASELINE.md) | The pre-expansion (six-crate) baseline this decomposition is grounded in |
| [`verification-forge/README.md`](./verification-forge/README.md) | The formal-verification workspace: architecture, invariants, roadmap |
| [`cloud-forge/README.md`](./cloud-forge/README.md) | The cloud-resource-substrate workspace: crate index, what's implemented |
| [`cloud-forge/docs/CLOUD_ARCHITECTURE.md`](./cloud-forge/docs/CLOUD_ARCHITECTURE.md) | The full 46-phase roadmap, layering, and Phase 1 scope decisions |
| [`tensor-forge/README.md`](./tensor-forge/README.md) | The tensor-library workspace: crate index, feature flags, quickstart, deliberate scope limits |
## License
This repository is dual-licensed:
1. **Open source:** the GNU Affero General Public License v3.0
(AGPLv3), reproduced verbatim in [`LICENSE-AGPL`](./LICENSE-AGPL).
Unless you have a signed commercial license (below), your use of
this code is governed solely by that file.
2. **Commercial:** a separately negotiated commercial license,
available as an alternative for parties who cannot or do not wish
to comply with the AGPLv3's copyleft terms. See
[`LICENSE-COMMERCIAL`](./LICENSE-COMMERCIAL) for the licensing
program template (a non-binding draft, not an executed agreement)
and contacts.
See [`LICENSE-NOTICE`](./LICENSE-NOTICE) for the copyright holder and
a summary of how the two licenses relate,
[`COPYRIGHT.md`](./COPYRIGHT.md) for the full copyright notice, and
[`TRADEMARKS.md`](./TRADEMARKS.md) for trademark terms (separate from
the copyright licenses above). `verification-forge/` and `cloud-forge/`
each carry their own identical copy of this same license set, since
either could be distributed independently of the root workspace.
### πŸ’Ό Commercial License
Snapkitty code is free and open under **AGPL-3.0** for open-source use. Building a commercial product or service? A **proprietary commercial license** from Snapkitty Collective LLC lets you ship this code without the AGPL's source-sharing and network-use obligations.
**[β†’ Get a commercial license](mailto:A.parr@belespritdaccord.uk?subject=Commercial%20license:%20tlm-jxcl-forge)** Β· A.parr@belespritdaccord.uk